harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/BoxIntegral/Basic.lean
theorem integral_nonneg {g : ℝⁿ → ℝ} (hg : ∀ x ∈ Box.Icc I, 0 ≤ g x) (μ : Measure ℝⁿ)
    [IsLocallyFiniteMeasure μ] : 0 ≤ integral I l g μ.toBoxAdditive.toSMul

Proof state:
case pos
ι : Type u
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
g : (ι → ℝ) → ℝ
hg : ∀ x ∈ Box.Icc I, 0 ≤ g x
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hgi : Integrable I l g μ.toBoxAdditive.toSMul
π : TaggedPrepartition I
J : Box ι
x✝ : J ∈ π.boxes
⊢ 0 ≤ (μ.toBoxAdditive.toSMul J) (g (π.tag J))

Tactic:
exact mul_nonneg ENNReal.toReal_nonneg (hg _ <| π.tag_mem_Icc _)

Result:
no goals

Proof state:
case pos
ι : Type u
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
g : (ι → ℝ) → ℝ
hg : ∀ x ∈ Box.Icc I, 0 ≤ g x
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hgi : Integrable I l g μ.toBoxAdditive.toSMul
⊢ 0 ≤ integral I l g μ.toBoxAdditive.toSMul

Tactic:
refine ge_of_tendsto' hgi.hasIntegral fun π => sum_nonneg fun J _ => ?_

Result:
case pos
ι : Type u
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
g : (ι → ℝ) → ℝ
hg : ∀ x ∈ Box.Icc I, 0 ≤ g x
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hgi : Integrable I l g μ.toBoxAdditive.toSMul
π : TaggedPrepartition I
J : Box ι
x✝ : J ∈ π.boxes
⊢ 0 ≤ (μ.toBoxAdditive.toSMul J) (g (π.tag J))

Proof state:
ι : Type u
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
g : (ι → ℝ) → ℝ
hg : ∀ x ∈ Box.Icc I, 0 ≤ g x
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ 0 ≤ integral I l g μ.toBoxAdditive.toSMul

Tactic:
by_cases hgi : Integrable I l g μ.toBoxAdditive.toSMul

Result:
case pos
ι : Type u
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
g : (ι → ℝ) → ℝ
hg : ∀ x ∈ Box.Icc I, 0 ≤ g x
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hgi : Integrable I l g μ.toBoxAdditive.toSMul
⊢ 0 ≤ integral I l g μ.toBoxAdditive.toSMul

case neg
ι : Type u
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
g : (ι → ℝ) → ℝ
hg : ∀ x ∈ Box.Icc I, 0 ≤ g x
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hgi : ¬Integrable I l g μ.toBoxAdditive.toSMul
⊢ 0 ≤ integral I l g μ.toBoxAdditive.toSMul

Proof state:
case neg
ι : Type u
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
g : (ι → ℝ) → ℝ
hg : ∀ x ∈ Box.Icc I, 0 ≤ g x
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hgi : ¬Integrable I l g μ.toBoxAdditive.toSMul
⊢ 0 ≤ integral I l g μ.toBoxAdditive.toSMul

Tactic:
rw [integral, dif_neg hgi]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem sdiff_sdiff_sup_sdiff : z \ (x \ y ⊔ y \ x) = z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ x) :=
  calc
    z \ (x \ y ⊔ y \ x) = (z \ x ⊔ z ⊓ x ⊓ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x)

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ z ⊓ z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ x) = z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ x)

Tactic:
rw [inf_idem]

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ z \ (x \ y ⊔ y \ x) = (z \ x ⊔ z ⊓ x ⊓ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x)

Tactic:
rw [sdiff_sup, sdiff_sdiff_right, sdiff_sdiff_right]

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ z ⊓ (z \ x ⊔ y) ⊓ (z ⊓ (z \ y ⊔ x)) = z ⊓ z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ x)

Tactic:
ac_rfl

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (z \ x ⊔ z ⊓ x ⊓ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x) = z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x)

Tactic:
rw [sup_inf_left, sup_comm, sup_inf_sdiff]

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x) = z ⊓ (z \ x ⊔ y) ⊓ (z ⊓ (z \ y ⊔ x))

Tactic:
rw [sup_inf_left, sup_comm (z \ y), sup_inf_sdiff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx?_isNone {xs : List α} {p : α → Bool} :
    (xs.findIdx? p).isNone = xs.all (¬p ·)

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : (findIdx? p xs).isNone = xs.all fun x => decide ¬p x = true
⊢ (if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs)).isNone =
    (x :: xs).all fun x => decide ¬p x = true

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
⊢ (findIdx? p []).isNone = [].all fun x => decide ¬p x = true

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : (findIdx? p xs).isNone = xs.all fun x => decide ¬p x = true
⊢ (findIdx? p (x :: xs)).isNone = (x :: xs).all fun x => decide ¬p x = true

Tactic:
simp only [findIdx?_cons]

Result:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : (findIdx? p xs).isNone = xs.all fun x => decide ¬p x = true
⊢ (if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs)).isNone =
    (x :: xs).all fun x => decide ¬p x = true

Proof state:
α : Type u_1
xs : List α
p : α → Bool
⊢ (findIdx? p xs).isNone = xs.all fun x => decide ¬p x = true

Tactic:
induction xs with
| nil => simp
| cons x xs ih =>
  simp only [findIdx?_cons]
  split <;> simp_all

Result:
no goals
-- Mathlib/Topology/Order/OrderClosed.lean
theorem Dense.exists_ge' {s : Set α} (hs : Dense s) (htop : ∀ x, IsTop x → x ∈ s) (x : α) :
    ∃ y ∈ s, x ≤ y

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
s : Set α
hs : Dense s
htop : ∀ (x : α), IsTop x → x ∈ s
x : α
⊢ ∃ y ∈ s, x ≤ y

Tactic:
by_cases hx : IsTop x

Result:
case pos
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
s : Set α
hs : Dense s
htop : ∀ (x : α), IsTop x → x ∈ s
x : α
hx : IsTop x
⊢ ∃ y ∈ s, x ≤ y

case neg
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
s : Set α
hs : Dense s
htop : ∀ (x : α), IsTop x → x ∈ s
x : α
hx : ¬IsTop x
⊢ ∃ y ∈ s, x ≤ y

Proof state:
case neg.intro.intro
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
s : Set α
hs : Dense s
htop : ∀ (x : α), IsTop x → x ∈ s
x : α
hx : ∃ x_1, x < x_1
y : α
hys : y ∈ s
hy : x < y
⊢ ∃ y ∈ s, x ≤ y

Tactic:
exact ⟨y, hys, hy.le⟩

Result:
no goals

Proof state:
case neg
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
s : Set α
hs : Dense s
htop : ∀ (x : α), IsTop x → x ∈ s
x : α
hx : ∃ x_1, x < x_1
⊢ ∃ y ∈ s, x ≤ y

Tactic:
rcases hs.exists_mem_open isOpen_Ioi hx with ⟨y, hys, hy : x < y⟩

Result:
case neg.intro.intro
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
s : Set α
hs : Dense s
htop : ∀ (x : α), IsTop x → x ∈ s
x : α
hx : ∃ x_1, x < x_1
y : α
hys : y ∈ s
hy : x < y
⊢ ∃ y ∈ s, x ≤ y

Proof state:
case pos
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
s : Set α
hs : Dense s
htop : ∀ (x : α), IsTop x → x ∈ s
x : α
hx : IsTop x
⊢ ∃ y ∈ s, x ≤ y

Tactic:
exact ⟨x, htop x hx, le_rfl⟩

Result:
no goals

Proof state:
case neg
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
s : Set α
hs : Dense s
htop : ∀ (x : α), IsTop x → x ∈ s
x : α
hx : ¬IsTop x
⊢ ∃ y ∈ s, x ≤ y

Tactic:
simp only [IsTop, not_forall, not_le] at hx

Result:
case neg
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
s : Set α
hs : Dense s
htop : ∀ (x : α), IsTop x → x ∈ s
x : α
hx : ∃ x_1, x < x_1
⊢ ∃ y ∈ s, x ≤ y
-- Mathlib/RingTheory/PowerSeries/Derivative.lean
theorem derivative_invOf {R} [CommRing R] (f : R⟦X⟧) [Invertible f] :
    d⁄dX R ⅟f = - ⅟f ^ 2 * d⁄dX R f

Proof state:
R : Type u_1
inst✝¹ : CommRing R
f : R⟦X⟧
inst✝ : Invertible f
⊢ (d⁄dX R) ⅟f = -⅟f ^ 2 * (d⁄dX R) f

Tactic:
rw [Derivation.leibniz_invOf, smul_eq_mul]

Result:
no goals
-- Mathlib/Analysis/Analytic/RadiusLiminf.lean
theorem radius_eq_liminf :
    p.radius = liminf (fun n => (1 / (‖p n‖₊ ^ (1 / (n : ℝ)) : ℝ≥0) : ℝ≥0∞)) atTop

Proof state:
case a.intro.intro.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : ↑r < p.radius
a : ℝ
ha : a ∈ Set.Ioo 0 1
H : ∀ᶠ (n : ℕ) in atTop, |‖p n‖ * ↑r ^ n| ≤ a ^ n
n : ℕ
hn₀ : 0 < n
hn : |‖p n‖ * ↑r ^ n| ≤ a ^ n
⊢ ‖p n‖ * ↑r ^ n ≤ 1

Tactic:
exact (le_abs_self _).trans (hn.trans (pow_le_one₀ ha.1.le ha.2.le))

Result:
no goals
-- Mathlib/Order/PiLex.lean
theorem le_toLex_update_self_iff : toLex x ≤ toLex (update x i a) ↔ x i ≤ a

Proof state:
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : (i : ι) → PartialOrder (β i)
x : (i : ι) → β i
i : ι
a : β i
⊢ toLex x ≤ toLex (update x i a) ↔ x i ≤ a

Tactic:
simp_rw [le_iff_lt_or_eq, lt_toLex_update_self_iff, toLex_inj, eq_update_self_iff]

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Ring.lean
theorem isJacobsonRing_polynomial_of_isJacobsonRing (hR : IsJacobsonRing R) :
    IsJacobsonRing R[X]

Proof state:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
f : R[X]
n : ℕ
hf : (map ((Ideal.Quotient.mk I).comp C).rangeRestrict f).coeff n = 0
⊢ f.coeff n ∈ comap C I

Tactic:
rw [coeff_map, Subtype.ext_iff] at hf

Result:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
f : R[X]
n : ℕ
hf : ↑(((Ideal.Quotient.mk I).comp C).rangeRestrict (f.coeff n)) = ↑0
⊢ f.coeff n ∈ comap C I

Proof state:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
⊢ ∀ (P : Ideal R[X]), P.IsPrime → P.jacobson = P

Tactic:
intro I hI

Result:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
⊢ I.jacobson = I

Proof state:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective ⇑(mapRingHom i)
this : J.IsPrime
h : J.jacobson = J
⊢ I.jacobson = I

Tactic:
replace h := congrArg (comap (Polynomial.mapRingHom i)) h

Result:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective ⇑(mapRingHom i)
this : J.IsPrime
h : comap (mapRingHom i) J.jacobson = comap (mapRingHom i) J
⊢ I.jacobson = I
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem equivAdjoinSimple_symm_gen (pb : PowerBasis K L) :
    pb.equivAdjoinSimple.symm pb.gen = AdjoinSimple.gen K pb.gen

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
pb : PowerBasis K L
⊢ pb.equivAdjoinSimple.symm pb.gen = AdjoinSimple.gen K pb.gen

Tactic:
rw [equivAdjoinSimple, equivOfMinpoly_symm, equivOfMinpoly_gen, adjoin.powerBasis_gen]

Result:
no goals
-- Mathlib/Order/Interval/Basic.lean
theorem toProd_injective : Injective (toProd : NonemptyInterval α → α × α) :=
  fun s t h => by cases s; cases t; congr

Proof state:
case mk.mk
α : Type u_1
inst✝ : LE α
toProd✝¹ : α × α
fst_le_snd✝¹ : toProd✝¹.1 ≤ toProd✝¹.2
toProd✝ : α × α
fst_le_snd✝ : toProd✝.1 ≤ toProd✝.2
h : { toProd := toProd✝¹, fst_le_snd := fst_le_snd✝¹ }.toProd = { toProd := toProd✝, fst_le_snd := fst_le_snd✝ }.toProd
⊢ { toProd := toProd✝¹, fst_le_snd := fst_le_snd✝¹ } = { toProd := toProd✝, fst_le_snd := fst_le_snd✝ }

Tactic:
congr

Result:
no goals

Proof state:
case mk
α : Type u_1
inst✝ : LE α
t : NonemptyInterval α
toProd✝ : α × α
fst_le_snd✝ : toProd✝.1 ≤ toProd✝.2
h : { toProd := toProd✝, fst_le_snd := fst_le_snd✝ }.toProd = t.toProd
⊢ { toProd := toProd✝, fst_le_snd := fst_le_snd✝ } = t

Tactic:
cases t

Result:
case mk.mk
α : Type u_1
inst✝ : LE α
toProd✝¹ : α × α
fst_le_snd✝¹ : toProd✝¹.1 ≤ toProd✝¹.2
toProd✝ : α × α
fst_le_snd✝ : toProd✝.1 ≤ toProd✝.2
h : { toProd := toProd✝¹, fst_le_snd := fst_le_snd✝¹ }.toProd = { toProd := toProd✝, fst_le_snd := fst_le_snd✝ }.toProd
⊢ { toProd := toProd✝¹, fst_le_snd := fst_le_snd✝¹ } = { toProd := toProd✝, fst_le_snd := fst_le_snd✝ }

Proof state:
α : Type u_1
inst✝ : LE α
s t : NonemptyInterval α
h : s.toProd = t.toProd
⊢ s = t

Tactic:
cases s

Result:
case mk
α : Type u_1
inst✝ : LE α
t : NonemptyInterval α
toProd✝ : α × α
fst_le_snd✝ : toProd✝.1 ≤ toProd✝.2
h : { toProd := toProd✝, fst_le_snd := fst_le_snd✝ }.toProd = t.toProd
⊢ { toProd := toProd✝, fst_le_snd := fst_le_snd✝ } = t
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_conj (x : ℂ) : arg (conj x) = if arg x = π then π else -arg x

Proof state:
case inr.inr.inr.inl
x : ℂ
hr : 0 < x.re
hi : x.im = 0
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π

Tactic:
simp [hr, hr.le, hr.le.not_lt]

Result:
no goals

Proof state:
case inl.inr.inr
x : ℂ
hr : x.re < 0
hi : 0 < x.im
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π

Tactic:
simp [hr, hr.not_le, hi.ne.symm, hi.le, not_le.2 hi, sub_eq_neg_add]

Result:
no goals
-- Mathlib/GroupTheory/SemidirectProduct.lean
theorem lift_unique (F : N ⋊[φ] G →* H) :
    F = lift (F.comp inl) (F.comp inr) fun _ ↦ by ext; simp [inl_aut]

Proof state:
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
F : N ⋊[φ] G →* H
⊢ F = lift (F.comp inl) (F.comp inr) ⋯

Tactic:
rw [DFunLike.ext_iff]

Result:
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
F : N ⋊[φ] G →* H
⊢ ∀ (x : N ⋊[φ] G), F x = (lift (F.comp inl) (F.comp inr) ⋯) x

Proof state:
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
F : N ⋊[φ] G →* H
⊢ ∀ (x : N ⋊[φ] G), F x = (lift (F.comp inl) (F.comp inr) ⋯) x

Tactic:
simp only [lift, MonoidHom.comp_apply, MonoidHom.coe_mk, OneHom.coe_mk, ← map_mul,
  inl_left_mul_inr_right, forall_const]

Result:
no goals

Proof state:
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
fn : N →* H
fg : G →* H
h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn
F : N ⋊[φ] G →* H
x✝ : G
⊢ (F.comp inl).comp (MulEquiv.toMonoidHom (φ x✝)) =
    (MulEquiv.toMonoidHom (MulAut.conj ((F.comp inr) x✝))).comp (F.comp inl)

Tactic:
ext

Result:
case h
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
fn : N →* H
fg : G →* H
h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn
F : N ⋊[φ] G →* H
x✝¹ : G
x✝ : N
⊢ ((F.comp inl).comp (MulEquiv.toMonoidHom (φ x✝¹))) x✝ =
    ((MulEquiv.toMonoidHom (MulAut.conj ((F.comp inr) x✝¹))).comp (F.comp inl)) x✝

Proof state:
case h
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
fn : N →* H
fg : G →* H
h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn
F : N ⋊[φ] G →* H
x✝¹ : G
x✝ : N
⊢ ((F.comp inl).comp (MulEquiv.toMonoidHom (φ x✝¹))) x✝ =
    ((MulEquiv.toMonoidHom (MulAut.conj ((F.comp inr) x✝¹))).comp (F.comp inl)) x✝

Tactic:
simp [inl_aut]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem IsPrefix.map {β} (f : α → β) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) : l₁.map f <+: l₂.map f

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l₁ l₂ : List α
h : l₁ <+: l₂
⊢ List.map f l₁ <+: List.map f l₂

Tactic:
obtain ⟨r, rfl⟩ := h

Result:
case intro
α : Type u_1
β : Type u_2
f : α → β
l₁ r : List α
⊢ List.map f l₁ <+: List.map f (l₁ ++ r)

Proof state:
case intro
α : Type u_1
β : Type u_2
f : α → β
l₁ r : List α
⊢ List.map f l₁ <+: List.map f (l₁ ++ r)

Tactic:
rw [map_append]

Result:
case intro
α : Type u_1
β : Type u_2
f : α → β
l₁ r : List α
⊢ List.map f l₁ <+: List.map f l₁ ++ List.map f r

Proof state:
case intro
α : Type u_1
β : Type u_2
f : α → β
l₁ r : List α
⊢ List.map f l₁ <+: List.map f l₁ ++ List.map f r

Tactic:
apply prefix_append

Result:
no goals
-- Mathlib/Data/Int/Cast/Lemmas.lean
theorem ext_int {f g : ℤ →* M} (h_neg_one : f (-1) = g (-1))
    (h_nat : f.comp Int.ofNatHom.toMonoidHom = g.comp Int.ofNatHom.toMonoidHom) : f = g

Proof state:
case h.negSucc.e_a
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : f (-1) = g (-1)
h_nat : f.comp ↑ofNatHom = g.comp ↑ofNatHom
x : ℕ
⊢ f (↑x + 1) = g (↑x + 1)

Tactic:
exact mod_cast (DFunLike.congr_fun h_nat (x + 1) :)

Result:
no goals

Proof state:
case h.negSucc
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : f (-1) = g (-1)
h_nat : f.comp ↑ofNatHom = g.comp ↑ofNatHom
x : ℕ
⊢ f -[x+1] = g -[x+1]

Tactic:
rw [Int.negSucc_eq, ← neg_one_mul, f.map_mul, g.map_mul]

Result:
case h.negSucc
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : f (-1) = g (-1)
h_nat : f.comp ↑ofNatHom = g.comp ↑ofNatHom
x : ℕ
⊢ f (-1) * f (↑x + 1) = g (-1) * g (↑x + 1)

Proof state:
case h.negSucc
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : f (-1) = g (-1)
h_nat : f.comp ↑ofNatHom = g.comp ↑ofNatHom
x : ℕ
⊢ f (-1) * f (↑x + 1) = g (-1) * g (↑x + 1)

Tactic:
congr 1

Result:
case h.negSucc.e_a
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : f (-1) = g (-1)
h_nat : f.comp ↑ofNatHom = g.comp ↑ofNatHom
x : ℕ
⊢ f (↑x + 1) = g (↑x + 1)

Proof state:
case h.ofNat
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : f (-1) = g (-1)
h_nat : f.comp ↑ofNatHom = g.comp ↑ofNatHom
x : ℕ
⊢ f (ofNat x) = g (ofNat x)

Tactic:
exact (DFunLike.congr_fun h_nat x :)

Result:
no goals

Proof state:
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : f (-1) = g (-1)
h_nat : f.comp ↑ofNatHom = g.comp ↑ofNatHom
⊢ f = g

Tactic:
ext (x | x)

Result:
case h.ofNat
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : f (-1) = g (-1)
h_nat : f.comp ↑ofNatHom = g.comp ↑ofNatHom
x : ℕ
⊢ f (ofNat x) = g (ofNat x)

case h.negSucc
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : f (-1) = g (-1)
h_nat : f.comp ↑ofNatHom = g.comp ↑ofNatHom
x : ℕ
⊢ f -[x+1] = g -[x+1]
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Erase.lean
theorem getElem_eraseIdx_of_ge (l : List α) (i : Nat) (j : Nat) (h : j < (l.eraseIdx i).length) (h' : i ≤ j) :
    (l.eraseIdx i)[j] = l[j + 1]'(by rw [length_eraseIdx] at h; split at h <;> omega)

Proof state:
α : Type u_1
l : List α
i j : Nat
h : j < (l.eraseIdx i).length
h' : i ≤ j
⊢ (l.eraseIdx i)[j] = l[j + 1]

Tactic:
rw [getElem_eraseIdx, dif_neg]

Result:
case hnc
α : Type u_1
l : List α
i j : Nat
h : j < (l.eraseIdx i).length
h' : i ≤ j
⊢ ¬j < i

Proof state:
α : Type ?u.15094
l : List α
i j : Nat
h : j < if i < l.length then l.length - 1 else l.length
h' : i ≤ j
⊢ j + 1 < l.length

Tactic:
split at h <;> omega

Result:
no goals

Proof state:
case hnc
α : Type u_1
l : List α
i j : Nat
h : j < (l.eraseIdx i).length
h' : i ≤ j
⊢ ¬j < i

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.15094
l : List α
i j : Nat
h : j < (l.eraseIdx i).length
h' : i ≤ j
⊢ j + 1 < l.length

Tactic:
rw [length_eraseIdx] at h

Result:
α : Type ?u.15094
l : List α
i j : Nat
h : j < if i < l.length then l.length - 1 else l.length
h' : i ≤ j
⊢ j + 1 < l.length
-- Mathlib/Analysis/Normed/Module/Convex.lean
theorem convex_closedBall (a : E) (r : ℝ) : Convex ℝ (Metric.closedBall a r)

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : E
r : ℝ
⊢ Convex ℝ (closedBall a r)

Tactic:
simpa only [Metric.closedBall, sep_univ] using (convexOn_univ_dist a).convex_le r

Result:
no goals
-- Mathlib/Data/List/InsertIdx.lean
theorem map_insertIdx (f : α → β) (l : List α) (n : ℕ) (a : α) :
    (insertIdx n a l).map f = insertIdx n (f a) (l.map f)

Proof state:
α : Type u
β : Type v
f : α → β
l : List α
n : ℕ
a : α
⊢ map f (insertIdx n a l) = insertIdx n (f a) (map f l)

Tactic:
simpa only [pmap_eq_map] using (insertIdx_pmap (fun a _ ↦ f a) (fun _ _ ↦ trivial) trivial).symm

Result:
no goals
-- Mathlib/Topology/UrysohnsLemma.lean
theorem exists_continuous_one_zero_of_isCompact [RegularSpace X] [LocallyCompactSpace X]
    {s t : Set X} (hs : IsCompact s) (ht : IsClosed t) (hd : Disjoint s t) :
    ∃ f : C(X, ℝ), EqOn f 1 s ∧ EqOn f 0 t ∧ HasCompactSupport f ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
f : X → ℝ
hf : Continuous f
hfs : EqOn (⇑{ toFun := f, continuous_toFun := hf }) 0 s
hft : EqOn (⇑{ toFun := f, continuous_toFun := hf }) 1 (interior k)ᶜ
h'f : ∀ (x : X), { toFun := f, continuous_toFun := hf } x ∈ Icc 0 1
A : t ⊆ (interior k)ᶜ
x : X
hx : x ∉ k
⊢ { toFun := fun x => 1 - f x, continuous_toFun := ⋯ } x = 0

Tactic:
simp only [ContinuousMap.coe_mk, sub_eq_zero]

Result:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
f : X → ℝ
hf : Continuous f
hfs : EqOn (⇑{ toFun := f, continuous_toFun := hf }) 0 s
hft : EqOn (⇑{ toFun := f, continuous_toFun := hf }) 1 (interior k)ᶜ
h'f : ∀ (x : X), { toFun := f, continuous_toFun := hf } x ∈ Icc 0 1
A : t ⊆ (interior k)ᶜ
x : X
hx : x ∉ k
⊢ 1 = f x

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
f : X → ℝ
hf : Continuous f
hfs : EqOn (⇑{ toFun := f, continuous_toFun := hf }) 0 s
hft : EqOn (⇑{ toFun := f, continuous_toFun := hf }) 1 (interior k)ᶜ
h'f : ∀ (x : X), { toFun := f, continuous_toFun := hf } x ∈ Icc 0 1
A : t ⊆ (interior k)ᶜ
x : X
hx : x ∈ interior k
⊢ x ∈ k

Tactic:
exact interior_subset hx

Result:
no goals
-- Mathlib/Topology/Irreducible.lean
theorem isClosed_of_mem_irreducibleComponents (s) (H : s ∈ irreducibleComponents X) :
    IsClosed s

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
H : s ∈ irreducibleComponents X
⊢ IsClosed s

Tactic:
rw [← closure_eq_iff_isClosed, eq_comm]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
H : s ∈ irreducibleComponents X
⊢ s = closure s

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
H : s ∈ irreducibleComponents X
⊢ s = closure s

Tactic:
exact subset_closure.antisymm (H.2 H.1.closure subset_closure)

Result:
no goals