harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Fin/Tuple/Basic.lean
lemma append_rev {m n} (xs : Fin m → α) (ys : Fin n → α) (i : Fin (m + n)) :
    append xs ys (rev i) = append (ys ∘ rev) (xs ∘ rev) (i.cast (Nat.add_comm ..))

Proof state:
case intro
α : Sort u_1
m n : ℕ
xs : Fin m → α
ys : Fin n → α
i : Fin (m + n)
⊢ append xs ys i = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ i.rev)

Tactic:
induction i using Fin.addCases

Result:
case intro.left
α : Sort u_1
m n : ℕ
xs : Fin m → α
ys : Fin n → α
i✝ : Fin m
⊢ append xs ys (castAdd n i✝) = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ (castAdd n i✝).rev)

case intro.right
α : Sort u_1
m n : ℕ
xs : Fin m → α
ys : Fin n → α
i✝ : Fin n
⊢ append xs ys (natAdd m i✝) = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ (natAdd m i✝).rev)

Proof state:
α : Sort u_1
m n : ℕ
xs : Fin m → α
ys : Fin n → α
i : Fin (m + n)
⊢ append xs ys i.rev = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ i)

Tactic:
rcases rev_surjective i with ⟨i, rfl⟩

Result:
case intro
α : Sort u_1
m n : ℕ
xs : Fin m → α
ys : Fin n → α
i : Fin (m + n)
⊢ append xs ys i.rev.rev = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ i.rev)

Proof state:
case intro.left
α : Sort u_1
m n : ℕ
xs : Fin m → α
ys : Fin n → α
i✝ : Fin m
⊢ append xs ys (castAdd n i✝) = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ (castAdd n i✝).rev)

Tactic:
simp [rev_castAdd]

Result:
no goals

Proof state:
case intro
α : Sort u_1
m n : ℕ
xs : Fin m → α
ys : Fin n → α
i : Fin (m + n)
⊢ append xs ys i.rev.rev = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ i.rev)

Tactic:
rw [rev_rev]

Result:
case intro
α : Sort u_1
m n : ℕ
xs : Fin m → α
ys : Fin n → α
i : Fin (m + n)
⊢ append xs ys i = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ i.rev)

Proof state:
case intro.right
α : Sort u_1
m n : ℕ
xs : Fin m → α
ys : Fin n → α
i✝ : Fin n
⊢ append xs ys (natAdd m i✝) = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ (natAdd m i✝).rev)

Tactic:
simp [cast_rev, rev_addNat]

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem _root_.Multiset.stronglyMeasurable_prod' (l : Multiset (α → M))
    (hl : ∀ f ∈ l, StronglyMeasurable f) : StronglyMeasurable l.prod

Proof state:
α : Type u_1
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
m : MeasurableSpace α
l : Multiset (α → M)
hl : ∀ f ∈ l, StronglyMeasurable f
⊢ StronglyMeasurable l.prod

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
m : MeasurableSpace α
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ f ∈ Quot.mk (⇑(List.isSetoid (α → M))) l, StronglyMeasurable f
⊢ StronglyMeasurable (Multiset.prod (Quot.mk (⇑(List.isSetoid (α → M))) l))

Proof state:
α : Type u_1
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
m : MeasurableSpace α
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ f ∈ Quot.mk (⇑(List.isSetoid (α → M))) l, StronglyMeasurable f
⊢ ∀ f ∈ l, StronglyMeasurable f

Tactic:
simpa using hl

Result:
no goals

Proof state:
case mk
α : Type u_1
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
m : MeasurableSpace α
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ f ∈ Quot.mk (⇑(List.isSetoid (α → M))) l, StronglyMeasurable f
⊢ StronglyMeasurable (Multiset.prod (Quot.mk (⇑(List.isSetoid (α → M))) l))

Tactic:
simpa using l.stronglyMeasurable_prod' (by simpa using hl)

Result:
no goals
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem zero_nadd : 0 ♯ a = a

Proof state:
a : Ordinal.{u}
⊢ 0 ♯ a = a

Tactic:
rw [nadd_comm, nadd_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem LinearMap.toMatrix_smulBasis_left {G} [Group G] [DistribMulAction G M₁]
    [SMulCommClass G R M₁] (g : G) (f : M₁ →ₗ[R] M₂) :
    LinearMap.toMatrix (g • v₁) v₂ f =
      LinearMap.toMatrix v₁ v₂ (f ∘ₗ DistribMulAction.toLinearMap _ _ g)

Proof state:
case a
R : Type u_1
inst✝¹⁰ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : Finite m
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
G : Type u_7
inst✝² : Group G
inst✝¹ : DistribMulAction G M₁
inst✝ : SMulCommClass G R M₁
g : G
f : M₁ →ₗ[R] M₂
i✝ : m
j✝ : n
⊢ (v₂.repr (f ((g • v₁) j✝))) i✝ = (v₂.repr ((f ∘ₗ DistribMulAction.toLinearMap R M₁ g) (v₁ j✝))) i✝

Tactic:
dsimp

Result:
no goals

Proof state:
case a
R : Type u_1
inst✝¹⁰ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : Finite m
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
G : Type u_7
inst✝² : Group G
inst✝¹ : DistribMulAction G M₁
inst✝ : SMulCommClass G R M₁
g : G
f : M₁ →ₗ[R] M₂
i✝ : m
j✝ : n
⊢ (toMatrix (g • v₁) v₂) f i✝ j✝ = (toMatrix v₁ v₂) (f ∘ₗ DistribMulAction.toLinearMap R M₁ g) i✝ j✝

Tactic:
rw [LinearMap.toMatrix_apply, LinearMap.toMatrix_apply]

Result:
case a
R : Type u_1
inst✝¹⁰ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : Finite m
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
G : Type u_7
inst✝² : Group G
inst✝¹ : DistribMulAction G M₁
inst✝ : SMulCommClass G R M₁
g : G
f : M₁ →ₗ[R] M₂
i✝ : m
j✝ : n
⊢ (v₂.repr (f ((g • v₁) j✝))) i✝ = (v₂.repr ((f ∘ₗ DistribMulAction.toLinearMap R M₁ g) (v₁ j✝))) i✝

Proof state:
R : Type u_1
inst✝¹⁰ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : Finite m
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
G : Type u_7
inst✝² : Group G
inst✝¹ : DistribMulAction G M₁
inst✝ : SMulCommClass G R M₁
g : G
f : M₁ →ₗ[R] M₂
⊢ (toMatrix (g • v₁) v₂) f = (toMatrix v₁ v₂) (f ∘ₗ DistribMulAction.toLinearMap R M₁ g)

Tactic:
ext

Result:
case a
R : Type u_1
inst✝¹⁰ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : Finite m
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
G : Type u_7
inst✝² : Group G
inst✝¹ : DistribMulAction G M₁
inst✝ : SMulCommClass G R M₁
g : G
f : M₁ →ₗ[R] M₂
i✝ : m
j✝ : n
⊢ (toMatrix (g • v₁) v₂) f i✝ j✝ = (toMatrix v₁ v₂) (f ∘ₗ DistribMulAction.toLinearMap R M₁ g) i✝ j✝
-- Mathlib/CategoryTheory/Category/Quiv.lean
@[simp]
lemma homOfEq_map_homOfEq {X Y : V} (f : X ⟶ Y) {X' Y' : V} (hX : X = X') (hY : Y = Y')
    {X'' Y'' : W} (hX' : e X' = X'') (hY' : e Y' = Y'') :
    Quiver.homOfEq (he _ _ (Quiver.homOfEq f hX hY)) hX' hY' =
      Quiver.homOfEq (he _ _ f) (by rw [hX, hX']) (by rw [hY, hY'])

Proof state:
V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)
X Y : V
f : X ⟶ Y
⊢ Quiver.homOfEq ((he X Y) (Quiver.homOfEq f ⋯ ⋯)) ⋯ ⋯ = Quiver.homOfEq ((he X Y) f) ⋯ ⋯

Tactic:
rfl

Result:
no goals

Proof state:
V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)
X Y : V
f : X ⟶ Y
X' Y' : V
hX : X = X'
hY : Y = Y'
X'' Y'' : W
hX' : e X' = X''
hY' : e Y' = Y''
⊢ Quiver.homOfEq ((he X' Y') (Quiver.homOfEq f hX hY)) hX' hY' = Quiver.homOfEq ((he X Y) f) ⋯ ⋯

Tactic:
subst hX hY hX' hY'

Result:
V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)
X Y : V
f : X ⟶ Y
⊢ Quiver.homOfEq ((he X Y) (Quiver.homOfEq f ⋯ ⋯)) ⋯ ⋯ = Quiver.homOfEq ((he X Y) f) ⋯ ⋯

Proof state:
V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)
X Y : V
f : X ⟶ Y
X' Y' : V
hX : X = X'
hY : Y = Y'
X'' Y'' : W
hX' : e X' = X''
hY' : e Y' = Y''
⊢ e X = X''

Tactic:
rw [hX, hX']

Result:
no goals

Proof state:
V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)
X Y : V
f : X ⟶ Y
X' Y' : V
hX : X = X'
hY : Y = Y'
X'' Y'' : W
hX' : e X' = X''
hY' : e Y' = Y''
⊢ e Y = Y''

Tactic:
rw [hY, hY']

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem ball_subset_thickening {x : X} {E : Set X} (hx : x ∈ E) (δ : ℝ) :
    ball x δ ⊆ thickening δ E :=
  Subset.trans (by simp [Subset.rfl]) (thickening_subset_of_subset δ <| singleton_subset_iff.mpr hx)

Proof state:
X : Type u
inst✝ : PseudoMetricSpace X
x : X
E : Set X
hx : x ∈ E
δ : ℝ
⊢ ball x δ ⊆ thickening δ {x}

Tactic:
simp [Subset.rfl]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Trim.lean
theorem trim_trim {m₁ m₂ : MeasurableSpace α} {hm₁₂ : m₁ ≤ m₂} {hm₂ : m₂ ≤ m0} :
    (μ.trim hm₂).trim hm₁₂ = μ.trim (hm₁₂.trans hm₂)

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m₁ m₂ : MeasurableSpace α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m0
t : Set α
ht : MeasurableSet t
⊢ ((μ.trim hm₂).trim hm₁₂) t = (μ.trim ⋯) t

Tactic:
rw [trim_measurableSet_eq hm₁₂ ht, trim_measurableSet_eq (hm₁₂.trans hm₂) ht,
  trim_measurableSet_eq hm₂ (hm₁₂ t ht)]

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m₁ m₂ : MeasurableSpace α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m0
⊢ (μ.trim hm₂).trim hm₁₂ = μ.trim ⋯

Tactic:
refine @Measure.ext _ m₁ _ _ (fun t ht => ?_)

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m₁ m₂ : MeasurableSpace α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m0
t : Set α
ht : MeasurableSet t
⊢ ((μ.trim hm₂).trim hm₁₂) t = (μ.trim ⋯) t
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem Ordered.balRight {l : RBNode α} {v : α} {r : RBNode α}
    (lv : l.All (cmpLT cmp · v)) (vr : r.All (cmpLT cmp v ·))
    (hl : l.Ordered cmp) (hr : r.Ordered cmp) : (balRight l v r).Ordered cmp

Proof state:
α : Type u_1
cmp : α → α → Ordering
l : RBNode α
v : α
r : RBNode α
lv : All (fun x => cmpLT cmp x v) l
vr : All (fun x => cmpLT cmp v x) r
hl : Ordered cmp l
hr : Ordered cmp r
⊢ Ordered cmp (r.reverse.balLeft v l.reverse).reverse

Tactic:
exact .reverse <| hr.reverse.balLeft
  ((All.reverse.2 vr).imp cmpLT.flip) ((All.reverse.2 lv).imp cmpLT.flip) hl.reverse

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
l : RBNode α
v : α
r : RBNode α
lv : All (fun x => cmpLT cmp x v) l
vr : All (fun x => cmpLT cmp v x) r
hl : Ordered cmp l
hr : Ordered cmp r
⊢ Ordered cmp (l.balRight v r)

Tactic:
rw [← reverse_reverse (balRight ..), reverse_balRight]

Result:
α : Type u_1
cmp : α → α → Ordering
l : RBNode α
v : α
r : RBNode α
lv : All (fun x => cmpLT cmp x v) l
vr : All (fun x => cmpLT cmp v x) r
hl : Ordered cmp l
hr : Ordered cmp r
⊢ Ordered cmp (r.reverse.balLeft v l.reverse).reverse
-- Mathlib/Topology/Basic.lean
theorem accPt_iff_nhds (x : X) (C : Set X) : AccPt x (𝓟 C) ↔ ∀ U ∈ 𝓝 x, ∃ y ∈ U ∩ C, y ≠ x

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
⊢ AccPt x (𝓟 C) ↔ ∀ U ∈ 𝓝 x, ∃ y ∈ U ∩ C, y ≠ x

Tactic:
simp [acc_principal_iff_cluster, clusterPt_principal_iff, Set.Nonempty, exists_prop, and_assoc,
  @and_comm (¬_ = x)]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Ring.lean
theorem Tendsto.atTop_mul_atBot₀ (hf : Tendsto f l atTop) (hg : Tendsto g l atBot) :
    Tendsto (fun x => f x * g x) l atBot

Proof state:
α : Type u_1
β : Type u_2
inst✝ : OrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atBot
⊢ Tendsto (fun x => f x * g x) l atBot

Tactic:
have := hf.atTop_mul_atTop₀ <| tendsto_neg_atBot_atTop.comp hg

Result:
α : Type u_1
β : Type u_2
inst✝ : OrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atBot
this : Tendsto (fun x => f x * (Neg.neg ∘ g) x) l atTop
⊢ Tendsto (fun x => f x * g x) l atBot

Proof state:
α : Type u_1
β : Type u_2
inst✝ : OrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atBot
this : Tendsto (fun x => f x * (Neg.neg ∘ g) x) l atTop
⊢ Tendsto (fun x => f x * g x) l atBot

Tactic:
simpa only [Function.comp_def, neg_mul_eq_mul_neg, neg_neg] using
  tendsto_neg_atTop_atBot.comp this

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
lemma dZero_comp_subtype : dZero A ∘ₗ A.ρ.invariants.subtype = 0

Proof state:
case h.mk.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A.V
hx✝ : x ∈ A.ρ.invariants
g : G
hx : (A.ρ g) x = x
⊢ (dZero A ∘ₗ A.ρ.invariants.subtype) ⟨x, hx✝⟩ g = 0 ⟨x, hx✝⟩ g

Tactic:
rw [← sub_eq_zero] at hx

Result:
case h.mk.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A.V
hx✝ : x ∈ A.ρ.invariants
g : G
hx : (A.ρ g) x - x = 0
⊢ (dZero A ∘ₗ A.ρ.invariants.subtype) ⟨x, hx✝⟩ g = 0 ⟨x, hx✝⟩ g

Proof state:
case h.mk.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A.V
hx✝ : x ∈ A.ρ.invariants
g : G
hx : (A.ρ g) x - x = 0
⊢ (dZero A ∘ₗ A.ρ.invariants.subtype) ⟨x, hx✝⟩ g = 0 ⟨x, hx✝⟩ g

Tactic:
exact hx

Result:
no goals

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ dZero A ∘ₗ A.ρ.invariants.subtype = 0

Tactic:
ext ⟨x, hx⟩ g

Result:
case h.mk.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A.V
hx : x ∈ A.ρ.invariants
g : G
⊢ (dZero A ∘ₗ A.ρ.invariants.subtype) ⟨x, hx⟩ g = 0 ⟨x, hx⟩ g

Proof state:
case h.mk.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A.V
hx : x ∈ A.ρ.invariants
g : G
⊢ (dZero A ∘ₗ A.ρ.invariants.subtype) ⟨x, hx⟩ g = 0 ⟨x, hx⟩ g

Tactic:
replace hx := hx g

Result:
case h.mk.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A.V
hx✝ : x ∈ A.ρ.invariants
g : G
hx : (A.ρ g) x = x
⊢ (dZero A ∘ₗ A.ρ.invariants.subtype) ⟨x, hx✝⟩ g = 0 ⟨x, hx✝⟩ g
-- Mathlib/Analysis/NormedSpace/Real.lean
theorem interior_closedBall' (x : E) (r : ℝ) : interior (closedBall x r) = ball x r

Proof state:
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
⊢ interior (closedBall x 0) = ball x 0

Tactic:
rw [closedBall_zero, ball_zero, interior_singleton]

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ interior (closedBall x r) = ball x r

Tactic:
rcases eq_or_ne r 0 with (rfl | hr)

Result:
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
⊢ interior (closedBall x 0) = ball x 0

case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : r ≠ 0
⊢ interior (closedBall x r) = ball x r

Proof state:
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : r ≠ 0
⊢ interior (closedBall x r) = ball x r

Tactic:
exact interior_closedBall x hr

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
lemma δ_zero_cochain_comp {n₂ : ℤ} (z₁ : Cochain F G 0) (z₂ : Cochain G K n₂)
    (m₂ : ℤ) (h₂ : n₂ + 1 = m₂) :
    δ n₂ m₂ (z₁.comp z₂ (zero_add n₂)) =
      z₁.comp (δ n₂ m₂ z₂) (zero_add m₂) +
      n₂.negOnePow • ((δ 0 1 z₁).comp z₂ (by rw [add_comm, h₂])) :=
  δ_comp z₁ z₂ (zero_add n₂) 1 m₂ m₂ h₂ (zero_add 1) h₂

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m n₂ : ℤ
z₁ : Cochain F G 0
z₂ : Cochain G K n₂
m₂ : ℤ
h₂ : n₂ + 1 = m₂
⊢ 1 + n₂ = m₂

Tactic:
rw [add_comm, h₂]

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
theorem csInf_lt_iff (hb : BddBelow s) (hs : s.Nonempty) : sInf s < a ↔ ∃ b ∈ s, b < a

Proof state:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
a : α
hb : BddBelow s
hs : s.Nonempty
⊢ sInf s < a ↔ ∃ b ∈ s, b < a

Tactic:
simpa only [not_le, not_forall₂, exists_prop] using (le_csInf_iff hb hs).not

Result:
no goals
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem eval₂_root (f : R[X]) : f.eval₂ (of f) (root f) = 0

Proof state:
R : Type u
inst✝ : CommRing R
f : R[X]
⊢ eval₂ (of f) (root f) f = 0

Tactic:
rw [← algebraMap_eq, ← aeval_def, aeval_eq, mk_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_one_eq_true_iff_self_eq_zero {i : Nat} :
    Nat.testBit 1 i = true ↔ i = 0

Proof state:
i : Nat
⊢ testBit 1 i = true ↔ i = 0

Tactic:
cases i <;> simp

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/RestrictScalars.lean
theorem hasFDerivAt_of_restrictScalars {g' : E →L[𝕜] F} (h : HasFDerivAt f g' x)
    (H : f'.restrictScalars 𝕜 = g') : HasFDerivAt f f' x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' E
inst✝⁴ : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
f' : E →L[𝕜'] F
x : E
g' : E →L[𝕜] F
h : HasFDerivAt f g' x
H : restrictScalars 𝕜 f' = g'
⊢ HasFDerivAt f f' x

Tactic:
rw [← H] at h

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' E
inst✝⁴ : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
f' : E →L[𝕜'] F
x : E
g' : E →L[𝕜] F
h : HasFDerivAt f (restrictScalars 𝕜 f') x
H : restrictScalars 𝕜 f' = g'
⊢ HasFDerivAt f f' x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' E
inst✝⁴ : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
f' : E →L[𝕜'] F
x : E
g' : E →L[𝕜] F
h : HasFDerivAt f (restrictScalars 𝕜 f') x
H : restrictScalars 𝕜 f' = g'
⊢ HasFDerivAt f f' x

Tactic:
exact .of_isLittleO h.isLittleO

Result:
no goals
-- Mathlib/Data/Finset/NoncommProd.lean
theorem noncommProd_insert_of_not_mem' [DecidableEq α] (s : Finset α) (a : α) (f : α → β) (comm)
    (ha : a ∉ s) :
    noncommProd (insert a s) f comm =
      noncommProd s f (comm.mono fun _ => mem_insert_of_mem) * f a

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
s : Finset α
a : α
f : α → β
comm : (↑(insert a s)).Pairwise (Commute on f)
ha : a ∉ s
⊢ (insert a s).noncommProd f comm = s.noncommProd f ⋯ * f a

Tactic:
simp only [← cons_eq_insert _ _ ha, noncommProd_cons']

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean
theorem squashGCF_eq_self_of_terminated (terminatedAt_n : TerminatedAt g n) :
    squashGCF g n = g

Proof state:
case succ.mk
K : Type u_1
inst✝ : DivisionRing K
n✝ : ℕ
h✝ : K
s✝ : Stream'.Seq (Pair K)
terminatedAt_n : { h := h✝, s := s✝ }.TerminatedAt (n✝ + 1)
⊢ squashSeq s✝ n✝ = s✝

Tactic:
exact squashSeq_eq_self_of_terminated terminatedAt_n

Result:
no goals

Proof state:
case zero
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
terminatedAt_n : g.s.get? 0 = none
⊢ g.squashGCF 0 = g

Tactic:
simp only [convs', squashGCF, convs'Aux, terminatedAt_n]

Result:
no goals

Proof state:
case succ.mk
K : Type u_1
inst✝ : DivisionRing K
n✝ : ℕ
h✝ : K
s✝ : Stream'.Seq (Pair K)
terminatedAt_n : { h := h✝, s := s✝ }.TerminatedAt (n✝ + 1)
⊢ { h := h✝, s := s✝ }.squashGCF (n✝ + 1) = { h := h✝, s := s✝ }

Tactic:
simp only [squashGCF, mk.injEq, true_and]

Result:
case succ.mk
K : Type u_1
inst✝ : DivisionRing K
n✝ : ℕ
h✝ : K
s✝ : Stream'.Seq (Pair K)
terminatedAt_n : { h := h✝, s := s✝ }.TerminatedAt (n✝ + 1)
⊢ squashSeq s✝ n✝ = s✝

Proof state:
case zero
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
terminatedAt_n : g.TerminatedAt 0
⊢ g.squashGCF 0 = g

Tactic:
change g.s.get? 0 = none at terminatedAt_n

Result:
case zero
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
terminatedAt_n : g.s.get? 0 = none
⊢ g.squashGCF 0 = g

Proof state:
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : DivisionRing K
terminatedAt_n : g.TerminatedAt n
⊢ g.squashGCF n = g

Tactic:
cases n with
| zero =>
  change g.s.get? 0 = none at terminatedAt_n
  simp only [convs', squashGCF, convs'Aux, terminatedAt_n]
| succ =>
  cases g
  simp only [squashGCF, mk.injEq, true_and]
  exact squashSeq_eq_self_of_terminated terminatedAt_n

Result:
no goals

Proof state:
case succ
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
n✝ : ℕ
terminatedAt_n : g.TerminatedAt (n✝ + 1)
⊢ g.squashGCF (n✝ + 1) = g

Tactic:
cases g

Result:
case succ.mk
K : Type u_1
inst✝ : DivisionRing K
n✝ : ℕ
h✝ : K
s✝ : Stream'.Seq (Pair K)
terminatedAt_n : { h := h✝, s := s✝ }.TerminatedAt (n✝ + 1)
⊢ { h := h✝, s := s✝ }.squashGCF (n✝ + 1) = { h := h✝, s := s✝ }
-- Mathlib/Data/Finset/Defs.lean
theorem eq_of_veq : ∀ {s t : Finset α}, s.1 = t.1 → s = t
  | ⟨s, _⟩, ⟨t, _⟩, h => by cases h; rfl

Proof state:
case refl
α : Type u_1
s : Multiset α
nodup✝¹ nodup✝ : s.Nodup
⊢ { val := s, nodup := nodup✝¹ } = { val := s, nodup := nodup✝ }

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
s : Multiset α
nodup✝¹ : s.Nodup
t : Multiset α
nodup✝ : t.Nodup
h : { val := s, nodup := nodup✝¹ }.val = { val := t, nodup := nodup✝ }.val
⊢ { val := s, nodup := nodup✝¹ } = { val := t, nodup := nodup✝ }

Tactic:
cases h

Result:
case refl
α : Type u_1
s : Multiset α
nodup✝¹ nodup✝ : s.Nodup
⊢ { val := s, nodup := nodup✝¹ } = { val := s, nodup := nodup✝ }
-- Mathlib/Data/Fintype/Sets.lean
theorem toFinset_compl [Fintype α] [Fintype (sᶜ : Set _)] : sᶜ.toFinset = s.toFinsetᶜ

Proof state:
case h
α : Type u_1
s : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype α
inst✝ : Fintype ↑sᶜ
a✝ : α
⊢ a✝ ∈ sᶜ.toFinset ↔ a✝ ∈ s.toFinsetᶜ

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
s : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype α
inst✝ : Fintype ↑sᶜ
⊢ sᶜ.toFinset = s.toFinsetᶜ

Tactic:
ext

Result:
case h
α : Type u_1
s : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype α
inst✝ : Fintype ↑sᶜ
a✝ : α
⊢ a✝ ∈ sᶜ.toFinset ↔ a✝ ∈ s.toFinsetᶜ
-- Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
theorem zero_apply {P : C} (Q : C) (a : P) : (0 : P ⟶ Q) a = 0 :=
  Quotient.inductionOn a fun a' => by
    rw [pseudoZero_def, pseudoApply_mk']
    simp

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
a : Pseudoelement P
a' : Over P
⊢ pseudoApply 0 ⟦a'⟧ = 0

Tactic:
rw [pseudoZero_def, pseudoApply_mk']

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
a : Pseudoelement P
a' : Over P
⊢ ⟦Over.mk (a'.hom ≫ 0)⟧ = ⟦Over.mk 0⟧

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
a : Pseudoelement P
a' : Over P
⊢ ⟦Over.mk (a'.hom ≫ 0)⟧ = ⟦Over.mk 0⟧

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
@[simp]
lemma restrictionLT_map {k₁ k₂ : Set.Iio i} (φ : k₁ ⟶ k₂) :
    (restrictionLT F hi).map φ = F.map (homOfLE (by simpa using leOfHom φ)) := rfl

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : PartialOrder J
j : J
F : ↑(Set.Iic j) ⥤ C
i : J
hi : i ≤ j
k₁ k₂ : ↑(Set.Iio i)
φ : k₁ ⟶ k₂
⊢ ⋯.functor.obj k₁ ≤ ⋯.functor.obj k₂

Tactic:
simpa using leOfHom φ

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem le_sup'_iff : a ≤ s.sup' H f ↔ ∃ b ∈ s, a ≤ f b

Proof state:
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ a ≤ s.sup' H f ↔ ∃ b ∈ s, a ≤ f b

Tactic:
rw [← WithBot.coe_le_coe, coe_sup', Finset.le_sup_iff (WithBot.bot_lt_coe a)]

Result:
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ (∃ b ∈ s, ↑a ≤ (WithBot.some ∘ f) b) ↔ ∃ b ∈ s, a ≤ f b

Proof state:
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ (∃ b ∈ s, ↑a ≤ (WithBot.some ∘ f) b) ↔ ∃ b ∈ s, a ≤ f b

Tactic:
exact exists_congr (fun _ => and_congr_right' WithBot.coe_le_coe)

Result:
no goals