harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/KummerDedekind.lean
private lemma f_symm_aux (hx : (conductor R x).comap (algebraMap R S) ⊔ I = ⊤)
    (hx' : IsIntegral R x) (Q : R[X]) :
    (f hx hx').symm (Q.map (Ideal.Quotient.mk I)) = Q.aeval x

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
Q : R[X]
⊢ (KummerDedekind.f hx hx')
      ((KummerDedekind.f hx hx').symm
        ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
          (Polynomial.map (Ideal.Quotient.mk I) Q))) =
    (KummerDedekind.f hx hx') ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q))

Tactic:
rw [f, AlgEquiv.toRingEquiv_eq_coe, RingEquiv.symm_trans_apply, RingEquiv.symm_symm,
  RingEquiv.coe_trans, Function.comp_apply, RingEquiv.symm_apply_apply,
  RingEquiv.symm_trans_apply, quotEquivOfEq_symm, quotEquivOfEq_mk]

Result:
case a
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
Q : R[X]
⊢ ((↑((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I)).trans (quotEquivOfEq ⋯))
      ((↑((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I)).symm
        ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R (adjoin.powerBasis' hx').gen)}))
          (Polynomial.map (Ideal.Quotient.mk I) Q))) =
    (⇑((↑((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I)).trans (quotEquivOfEq ⋯)) ∘
        ⇑(quotAdjoinEquivQuotMap hx ⋯).symm)
      ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q))
-- Mathlib/CategoryTheory/Abelian/Images.lean
theorem coimageImageComparison_eq_coimageImageComparison' :
    coimageImageComparison f = coimageImageComparison' f

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
P Q : C
f : P ⟶ Q
⊢ coimageImageComparison f = coimageImageComparison' f

Tactic:
ext

Result:
case h.h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
P Q : C
f : P ⟶ Q
⊢ (coequalizer.π (kernel.ι f) 0 ≫ coimageImageComparison f) ≫ equalizer.ι (cokernel.π f) 0 =
    (coequalizer.π (kernel.ι f) 0 ≫ coimageImageComparison' f) ≫ equalizer.ι (cokernel.π f) 0

Proof state:
case h.h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
P Q : C
f : P ⟶ Q
⊢ (coequalizer.π (kernel.ι f) 0 ≫ coimageImageComparison f) ≫ equalizer.ι (cokernel.π f) 0 =
    (coequalizer.π (kernel.ι f) 0 ≫ coimageImageComparison' f) ≫ equalizer.ι (cokernel.π f) 0

Tactic:
simp [coimageImageComparison, coimageImageComparison']

Result:
no goals
-- Mathlib/Analysis/Fourier/FourierTransform.lean
lemma fourierIntegralInv_eq' (f : V → E) (w : V) :
    𝓕⁻ f w = ∫ v, Complex.exp ((↑(2 * π * ⟪v, w⟫) * Complex.I)) • f v

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : V → E
w : V
⊢ 𝓕⁻ f w = ∫ (v : V), Complex.exp (↑(2 * π * inner v w) * Complex.I) • f v

Tactic:
simp_rw [fourierIntegralInv_eq, Circle.smul_def, Real.fourierChar_apply]

Result:
no goals
-- Mathlib/Topology/Homotopy/Contractible.lean
theorem Nullhomotopic.comp_right {f : C(X, Y)} (hf : f.Nullhomotopic) (g : C(Y, Z)) :
    (g.comp f).Nullhomotopic

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
hf : f.Nullhomotopic
g : C(Y, Z)
⊢ (g.comp f).Nullhomotopic

Tactic:
obtain ⟨y, hy⟩ := hf

Result:
case intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
g : C(Y, Z)
y : Y
hy : f.Homotopic (const X y)
⊢ (g.comp f).Nullhomotopic

Proof state:
case intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
g : C(Y, Z)
y : Y
hy : f.Homotopic (const X y)
⊢ (g.comp f).Nullhomotopic

Tactic:
use g y

Result:
case h
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
g : C(Y, Z)
y : Y
hy : f.Homotopic (const X y)
⊢ (g.comp f).Homotopic (const X (g y))

Proof state:
case h
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
g : C(Y, Z)
y : Y
hy : f.Homotopic (const X y)
⊢ (g.comp f).Homotopic (const X (g y))

Tactic:
exact Homotopic.hcomp hy (Homotopic.refl g)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem tendsto_cos_pi_div_two : Tendsto cos (𝓝[<] (π / 2)) (𝓝[>] 0)

Proof state:
case h2

⊢ ∀ᶠ (x : ℝ) in 𝓝[<] (π / 2), cos x ∈ Ioi 0

Tactic:
filter_upwards [Ioo_mem_nhdsLT (neg_lt_self pi_div_two_pos)] with x hx

Result:
case h
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ cos x ∈ Ioi 0

Proof state:
⊢ Tendsto cos (𝓝[<] (π / 2)) (𝓝[>] 0)

Tactic:
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within

Result:
case h1

⊢ Tendsto cos (𝓝[<] (π / 2)) (𝓝 0)

case h2

⊢ ∀ᶠ (x : ℝ) in 𝓝[<] (π / 2), cos x ∈ Ioi 0

Proof state:
case h1

⊢ Tendsto cos (𝓝[<] (π / 2)) (𝓝 0)

Tactic:
convert continuous_cos.continuousWithinAt.tendsto

Result:
case h.e'_5.h.e'_3

⊢ 0 = cos (π / 2)

Proof state:
case h
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ cos x ∈ Ioi 0

Tactic:
exact cos_pos_of_mem_Ioo hx

Result:
no goals

Proof state:
case h.e'_5.h.e'_3

⊢ 0 = cos (π / 2)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/Homotopy.lean
theorem prevD_comp_right (f : ∀ i j, C.X i ⟶ D.X j) (g : D ⟶ E) (j : ι) :
    (prevD j fun i j => f i j ≫ g.f j) = prevD j f ≫ g.f j

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f : (i j : ι) → C.X i ⟶ D.X j
g : D ⟶ E
j : ι
⊢ ((prevD j) fun i j => f i j ≫ g.f j) = (prevD j) f ≫ g.f j

Tactic:
dsimp [prevD]

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f : (i j : ι) → C.X i ⟶ D.X j
g : D ⟶ E
j : ι
⊢ (f j (c.prev j) ≫ g.f (c.prev j)) ≫ E.d (c.prev j) j = (f j (c.prev j) ≫ D.d (c.prev j) j) ≫ g.f j

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f : (i j : ι) → C.X i ⟶ D.X j
g : D ⟶ E
j : ι
⊢ (f j (c.prev j) ≫ g.f (c.prev j)) ≫ E.d (c.prev j) j = (f j (c.prev j) ≫ D.d (c.prev j) j) ≫ g.f j

Tactic:
simp only [assoc, g.comm]

Result:
no goals
-- Mathlib/Data/Multiset/ZeroCons.lean
@[simp] lemma singleton_subset : {a} ⊆ s ↔ a ∈ s

Proof state:
α : Type u_1
s : Multiset α
a : α
⊢ {a} ⊆ s ↔ a ∈ s

Tactic:
simp [subset_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem get_find?_mem (xs : List α) (p : α → Bool) (h) : (xs.find? p).get h ∈ xs

Proof state:
case neg.a
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ (h : (find? p xs).isSome = true), (find? p xs).get h ∈ xs
h✝ : (find? p (x :: xs)).isSome = true
h : ¬p x = true
⊢ Mem ((find? p xs).get ⋯) xs

Tactic:
apply ih

Result:
no goals

Proof state:
case neg
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ (h : (find? p xs).isSome = true), (find? p xs).get h ∈ xs
h✝ : (find? p (x :: xs)).isSome = true
h : ¬p x = true
⊢ (find? p xs).get ⋯ ∈ x :: xs

Tactic:
right

Result:
case neg.a
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ (h : (find? p xs).isSome = true), (find? p xs).get h ∈ xs
h✝ : (find? p (x :: xs)).isSome = true
h : ¬p x = true
⊢ Mem ((find? p xs).get ⋯) xs

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ (h : (find? p xs).isSome = true), (find? p xs).get h ∈ xs
h : (find? p (x :: xs)).isSome = true
⊢ (find? p (x :: xs)).get h ∈ x :: xs

Tactic:
simp only [find?_cons]

Result:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ (h : (find? p xs).isSome = true), (find? p xs).get h ∈ xs
h : (find? p (x :: xs)).isSome = true
⊢ (match p x with
        | true => some x
        | false => find? p xs).get
      ⋯ ∈
    x :: xs

Proof state:
case nil
α : Type u_1
p : α → Bool
h : (find? p []).isSome = true
⊢ (find? p []).get h ∈ []

Tactic:
simp at h

Result:
no goals

Proof state:
case neg
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ (h : (find? p xs).isSome = true), (find? p xs).get h ∈ xs
h✝ : (find? p (x :: xs)).isSome = true
h : ¬p x = true
⊢ (match p x with
        | true => some x
        | false => find? p xs).get
      ⋯ ∈
    x :: xs

Tactic:
simp only [h]

Result:
case neg
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ (h : (find? p xs).isSome = true), (find? p xs).get h ∈ xs
h✝ : (find? p (x :: xs)).isSome = true
h : ¬p x = true
⊢ (find? p xs).get ⋯ ∈ x :: xs

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ (h : (find? p xs).isSome = true), (find? p xs).get h ∈ xs
h : (find? p (x :: xs)).isSome = true
⊢ (match p x with
        | true => some x
        | false => find? p xs).get
      ⋯ ∈
    x :: xs

Tactic:
by_cases h : p x

Result:
case pos
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ (h : (find? p xs).isSome = true), (find? p xs).get h ∈ xs
h✝ : (find? p (x :: xs)).isSome = true
h : p x = true
⊢ (match p x with
        | true => some x
        | false => find? p xs).get
      ⋯ ∈
    x :: xs

case neg
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ (h : (find? p xs).isSome = true), (find? p xs).get h ∈ xs
h✝ : (find? p (x :: xs)).isSome = true
h : ¬p x = true
⊢ (match p x with
        | true => some x
        | false => find? p xs).get
      ⋯ ∈
    x :: xs

Proof state:
case pos
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ (h : (find? p xs).isSome = true), (find? p xs).get h ∈ xs
h✝ : (find? p (x :: xs)).isSome = true
h : p x = true
⊢ (match p x with
        | true => some x
        | false => find? p xs).get
      ⋯ ∈
    x :: xs

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivativeFinsupp_map [Semiring S] (p : R[X]) (f : R →+* S) :
    derivativeFinsupp (p.map f) = (derivativeFinsupp p).mapRange (·.map f) (by simp)

Proof state:
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
⊢ (fun x => map f x) 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
case h
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
i : ℕ
⊢ (derivativeFinsupp (map f p)) i = (Finsupp.mapRange (fun x => map f x) ⋯ (derivativeFinsupp p)) i

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
⊢ derivativeFinsupp (map f p) = Finsupp.mapRange (fun x => map f x) ⋯ (derivativeFinsupp p)

Tactic:
ext i : 1

Result:
case h
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
i : ℕ
⊢ (derivativeFinsupp (map f p)) i = (Finsupp.mapRange (fun x => map f x) ⋯ (derivativeFinsupp p)) i
-- Mathlib/Analysis/Normed/Ring/SmoothingSeminorm.lean
theorem tendsto_smoothingFun_of_map_one_le_one (hμ1 : μ 1 ≤ 1) (x : R) :
    Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x))

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
⊢ Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x))

Tactic:
by_cases hx : μ x = 0

Result:
case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : μ x = 0
⊢ Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x))

case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ¬μ x = 0
⊢ Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x))

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ¬μ x = 0
⊢ Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x))

Tactic:
exact tendsto_smoothingFun_of_ne_zero μ hμ1 hx

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : μ x = 0
⊢ Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x))

Tactic:
exact tendsto_smoothingFun_of_eq_zero μ hx

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem map_set {f : α → β} {l : Vector α n} {i : Nat} {h : i < n} {a : α} :
    (l.set i a).map f = (l.map f).set i (f a) (by simpa using h)

Proof state:
case mk
α : Type u_1
β : Type u_2
n : Nat
f : α → β
i : Nat
h : i < n
a : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ map f ({ toArray := toArray✝, size_toArray := size_toArray✝ }.set i a h) =
    (map f { toArray := toArray✝, size_toArray := size_toArray✝ }).set i (f a) h

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.191275
β : Type ?u.191302
n : Nat
f : α → β
l : Vector α n
i : Nat
h : i < n
a : α
⊢ i < n

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
n : Nat
f : α → β
l : Vector α n
i : Nat
h : i < n
a : α
⊢ map f (l.set i a h) = (map f l).set i (f a) h

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
n : Nat
f : α → β
i : Nat
h : i < n
a : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ map f ({ toArray := toArray✝, size_toArray := size_toArray✝ }.set i a h) =
    (map f { toArray := toArray✝, size_toArray := size_toArray✝ }).set i (f a) h
-- Mathlib/Algebra/Lie/Solvable.lean
theorem derivedSeries_eq_derivedSeriesOfIdeal_comap (k : ℕ) :
    derivedSeries R I k = (derivedSeriesOfIdeal R L k I).comap I.incl

Proof state:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : derivedSeries R (↥I) k = comap I.incl (derivedSeriesOfIdeal R L k I)
⊢ derivedSeries R (↥I) (k + 1) = comap I.incl (derivedSeriesOfIdeal R L (k + 1) I)

Tactic:
simp only [derivedSeries_def, derivedSeriesOfIdeal_succ] at ih ⊢

Result:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : derivedSeriesOfIdeal R (↥I) k ⊤ = comap I.incl (derivedSeriesOfIdeal R L k I)
⊢ ⁅derivedSeriesOfIdeal R (↥I) k ⊤, derivedSeriesOfIdeal R (↥I) k ⊤⁆ =
    comap I.incl ⁅derivedSeriesOfIdeal R L k I, derivedSeriesOfIdeal R L k I⁆

Proof state:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : derivedSeriesOfIdeal R (↥I) k ⊤ = comap I.incl (derivedSeriesOfIdeal R L k I)
⊢ ⁅derivedSeriesOfIdeal R (↥I) k ⊤, derivedSeriesOfIdeal R (↥I) k ⊤⁆ =
    comap I.incl ⁅derivedSeriesOfIdeal R L k I, derivedSeriesOfIdeal R L k I⁆

Tactic:
rw [ih]

Result:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : derivedSeriesOfIdeal R (↥I) k ⊤ = comap I.incl (derivedSeriesOfIdeal R L k I)
⊢ ⁅comap I.incl (derivedSeriesOfIdeal R L k I), comap I.incl (derivedSeriesOfIdeal R L k I)⁆ =
    comap I.incl ⁅derivedSeriesOfIdeal R L k I, derivedSeriesOfIdeal R L k I⁆

Proof state:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : derivedSeriesOfIdeal R (↥I) k ⊤ = comap I.incl (derivedSeriesOfIdeal R L k I)
⊢ ⁅comap I.incl (derivedSeriesOfIdeal R L k I), comap I.incl (derivedSeriesOfIdeal R L k I)⁆ =
    comap I.incl ⁅derivedSeriesOfIdeal R L k I, derivedSeriesOfIdeal R L k I⁆

Tactic:
exact comap_bracket_incl_of_le I (derivedSeriesOfIdeal_le_self I k)
  (derivedSeriesOfIdeal_le_self I k)

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
⊢ derivedSeries R (↥I) k = comap I.incl (derivedSeriesOfIdeal R L k I)

Tactic:
induction k with
| zero => simp only [derivedSeries_def, comap_incl_self, derivedSeriesOfIdeal_zero]
| succ k ih =>
  simp only [derivedSeries_def, derivedSeriesOfIdeal_succ] at ih ⊢; rw [ih]
  exact comap_bracket_incl_of_le I (derivedSeriesOfIdeal_le_self I k)
    (derivedSeriesOfIdeal_le_self I k)

Result:
no goals

Proof state:
case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ derivedSeries R (↥I) 0 = comap I.incl (derivedSeriesOfIdeal R L 0 I)

Tactic:
simp only [derivedSeries_def, comap_incl_self, derivedSeriesOfIdeal_zero]

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem nextOr_cons_of_ne (xs : List α) (y x d : α) (h : x ≠ y) :
    nextOr (y :: xs) x d = nextOr xs x d

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs : List α
y x d : α
h : x ≠ y
⊢ (y :: xs).nextOr x d = xs.nextOr x d

Tactic:
rcases xs with - | ⟨z, zs⟩

Result:
case nil
α : Type u_1
inst✝ : DecidableEq α
y x d : α
h : x ≠ y
⊢ [y].nextOr x d = [].nextOr x d

case cons
α : Type u_1
inst✝ : DecidableEq α
y x d : α
h : x ≠ y
z : α
zs : List α
⊢ (y :: z :: zs).nextOr x d = (z :: zs).nextOr x d

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
y x d : α
h : x ≠ y
⊢ [y].nextOr x d = [].nextOr x d

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
y x d : α
h : x ≠ y
z : α
zs : List α
⊢ (y :: z :: zs).nextOr x d = (z :: zs).nextOr x d

Tactic:
exact if_neg h

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem top_prod (H : Subgroup N) : (⊤ : Subgroup G).prod H = H.comap (MonoidHom.snd G N) :=
  ext fun x => by simp [mem_prod, MonoidHom.coe_snd]

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup N
x : G × N
⊢ x ∈ ⊤.prod H ↔ x ∈ comap (MonoidHom.snd G N) H

Tactic:
simp [mem_prod, MonoidHom.coe_snd]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem limit.lift_extend {F : J ⥤ C} [HasLimit F] (c : Cone F) {X : C} (f : X ⟶ c.pt) :
    limit.lift F (c.extend f) = f ≫ limit.lift F c

Proof state:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimit F
c : Cone F
X : C
f : X ⟶ c.pt
⊢ lift F (c.extend f) = f ≫ lift F c

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Fold.lean
theorem dfoldlM_loop [Monad m] (f : (i : Fin (n+1)) → α i.castSucc → m (α i.succ)) (h : i < n+1)
    (x) : dfoldlM.loop (n+1) α f i (Nat.lt_add_right 1 h) x =
      f ⟨i, h⟩ x >>= (dfoldlM.loop n (α ∘ succ) (f ·.succ ·) i h .)

Proof state:
case refl
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
inst✝ : Monad m
f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ)
h : n < n + 1
x : α ⟨n, ⋯⟩
h' : ¬n < n
⊢ dfoldlM.loop (n + 1) α f n ⋯ x = do
    let x ← f ⟨n, h⟩ x
    dfoldlM.loop n (α ∘ succ) (fun x1 x2 => f x1.succ x2) n h x

Tactic:
rw [dfoldlM_loop_lt]

Result:
case refl
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
inst✝ : Monad m
f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ)
h : n < n + 1
x : α ⟨n, ⋯⟩
h' : ¬n < n
⊢ f ⟨n, ?refl.h⟩ x >>= dfoldlM.loop (n + 1) α f (n + 1) ⋯ = do
    let x ← f ⟨n, h⟩ x
    dfoldlM.loop n (α ∘ succ) (fun x1 x2 => f x1.succ x2) n h x

case refl.h
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
inst✝ : Monad m
f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ)
h : n < n + 1
x : α ⟨n, ⋯⟩
h' : ¬n < n
⊢ n < n + 1
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem dist_log_im_le (z w : ℍ) : dist (log z.im) (log w.im) ≤ dist z w :=
  calc
    dist (log z.im) (log w.im) = dist (mk ⟨0, z.im⟩ z.im_pos) (mk ⟨0, w.im⟩ w.im_pos) :=
      Eq.symm <| dist_of_re_eq rfl
    _ ≤ dist z w

Proof state:
case h.a.hab
z w : ℍ
⊢ dist { re := 0, im := z.im } { re := 0, im := w.im } ≤ dist ↑z ↑w

Tactic:
simpa [sqrt_sq_eq_abs] using Complex.abs_im_le_norm (z - w)

Result:
no goals

Proof state:
z w : ℍ
⊢ 2 *
      arsinh
        (dist ↑(mk { re := 0, im := z.im } ⋯) ↑(mk { re := 0, im := w.im } ⋯) /
          (2 * √((mk { re := 0, im := z.im } ⋯).im * (mk { re := 0, im := w.im } ⋯).im))) ≤
    2 * arsinh (dist ↑z ↑w / (2 * √(z.im * w.im)))

Tactic:
dsimp only [coe_mk, mk_im]

Result:
z w : ℍ
⊢ 2 * arsinh (dist { re := 0, im := z.im } { re := 0, im := w.im } / (2 * √(z.im * w.im))) ≤
    2 * arsinh (dist ↑z ↑w / (2 * √(z.im * w.im)))

Proof state:
z w : ℍ
⊢ 2 * arsinh (dist { re := 0, im := z.im } { re := 0, im := w.im } / (2 * √(z.im * w.im))) ≤
    2 * arsinh (dist ↑z ↑w / (2 * √(z.im * w.im)))

Tactic:
gcongr

Result:
case h.a.hab
z w : ℍ
⊢ dist { re := 0, im := z.im } { re := 0, im := w.im } ≤ dist ↑z ↑w

Proof state:
z w : ℍ
⊢ dist (mk { re := 0, im := z.im } ⋯) (mk { re := 0, im := w.im } ⋯) ≤ dist z w

Tactic:
simp_rw [dist_eq]

Result:
z w : ℍ
⊢ 2 *
      arsinh
        (dist ↑(mk { re := 0, im := z.im } ⋯) ↑(mk { re := 0, im := w.im } ⋯) /
          (2 * √((mk { re := 0, im := z.im } ⋯).im * (mk { re := 0, im := w.im } ⋯).im))) ≤
    2 * arsinh (dist ↑z ↑w / (2 * √(z.im * w.im)))
-- Mathlib/Algebra/ModEq.lean
theorem modEq_sub_iff_add_modEq : a ≡ b - c [PMOD p] ↔ a + c ≡ b [PMOD p] :=
  modEq_sub_iff_add_modEq'.trans <| by rw [add_comm]

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
p a b c : α
⊢ c + a ≡ b [PMOD p] ↔ a + c ≡ b [PMOD p]

Tactic:
rw [add_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem sshiftRight_xor_distrib (x y : BitVec w) (n : Nat) :
    (x ^^^ y).sshiftRight n = (x.sshiftRight n) ^^^ (y.sshiftRight n)

Proof state:
w : Nat
x y : BitVec w
n : Nat
⊢ (x ^^^ y).sshiftRight n = x.sshiftRight n ^^^ y.sshiftRight n

Tactic:
ext i

Result:
case pred
w : Nat
x y : BitVec w
n i : Nat
a✝ : i < w
⊢ ((x ^^^ y).sshiftRight n).getLsbD i = (x.sshiftRight n ^^^ y.sshiftRight n).getLsbD i

Proof state:
case pred
w : Nat
x y : BitVec w
n i : Nat
a✝ : i < w
⊢ ((x ^^^ y).sshiftRight n).getLsbD i = (x.sshiftRight n ^^^ y.sshiftRight n).getLsbD i

Tactic:
simp only [getLsbD_sshiftRight, getLsbD_xor, msb_xor]

Result:
case pred
w : Nat
x y : BitVec w
n i : Nat
a✝ : i < w
⊢ (!decide (w ≤ i) && if n + i < w then x.getLsbD (n + i) ^^ y.getLsbD (n + i) else x.msb ^^ y.msb) =
    ((!decide (w ≤ i) && if n + i < w then x.getLsbD (n + i) else x.msb) ^^
      !decide (w ≤ i) && if n + i < w then y.getLsbD (n + i) else y.msb)

Proof state:
case pred
w : Nat
x y : BitVec w
n i : Nat
a✝ : i < w
⊢ (!decide (w ≤ i) && if n + i < w then x.getLsbD (n + i) ^^ y.getLsbD (n + i) else x.msb ^^ y.msb) =
    ((!decide (w ≤ i) && if n + i < w then x.getLsbD (n + i) else x.msb) ^^
      !decide (w ≤ i) && if n + i < w then y.getLsbD (n + i) else y.msb)

Tactic:
split
  <;> by_cases w ≤ i
  <;> simp [*]

Result:
no goals
-- Mathlib/RingTheory/Congruence/Basic.lean
theorem sSup_def {S : Set (RingCon R)} :
    sSup S = ringConGen (sSup (@Set.image (RingCon R) (R → R → Prop) (⇑) S))

Proof state:
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
⊢ sSup S = ringConGen (sSup (DFunLike.coe '' S))

Tactic:
rw [sSup_eq_ringConGen, sSup_image]

Result:
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
⊢ (ringConGen fun x y => ∃ c ∈ S, c x y) = ringConGen (⨆ a ∈ S, ⇑a)

Proof state:
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
⊢ (ringConGen fun x y => ∃ c ∈ S, c x y) = ringConGen (⨆ a ∈ S, ⇑a)

Tactic:
congr with (x y)

Result:
case e_r.h.h.a
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
x y : R
⊢ (∃ c ∈ S, c x y) ↔ (⨆ a ∈ S, ⇑a) x y

Proof state:
case e_r.h.h.a
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
x y : R
⊢ (∃ c ∈ S, c x y) ↔ (⨆ a ∈ S, ⇑a) x y

Tactic:
simp only [sSup_image, iSup_apply, iSup_Prop_eq, exists_prop, rel_eq_coe]

Result:
no goals