harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/Composition/Comp.lean
@[simp]
lemma swap_copy : (swap α α) ∘ₖ (copy α) = copy α

Proof state:
α : Type u_1
mα : MeasurableSpace α
⊢ swap α α ∘ₖ copy α = copy α

Tactic:
ext a s hs

Result:
case h.h
α : Type u_1
mα : MeasurableSpace α
a : α
s : Set (α × α)
hs : MeasurableSet s
⊢ ((swap α α ∘ₖ copy α) a) s = ((copy α) a) s

Proof state:
case h.h
α : Type u_1
mα : MeasurableSpace α
a : α
s : Set (α × α)
hs : MeasurableSet s
⊢ ((swap α α ∘ₖ copy α) a) s = ((copy α) a) s

Tactic:
rw [comp_apply, copy_apply, Measure.dirac_bind (Kernel.measurable _), swap_apply' _ hs,
  Measure.dirac_apply' _ hs]

Result:
case h.h
α : Type u_1
mα : MeasurableSpace α
a : α
s : Set (α × α)
hs : MeasurableSet s
⊢ s.indicator 1 (a, a).swap = s.indicator 1 (a, a)

Proof state:
case h.h
α : Type u_1
mα : MeasurableSpace α
a : α
s : Set (α × α)
hs : MeasurableSet s
⊢ s.indicator 1 (a, a).swap = s.indicator 1 (a, a)

Tactic:
congr

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem iUnion_of_monotone_of_frequently
    {ι : Type*} [Preorder ι] [(atTop : Filter ι).IsCountablyGenerated] {s : ι → Set α}
    (hsm : Monotone s) (hs : ∃ᶠ i in atTop, MeasurableSet (s i)) : MeasurableSet (⋃ i, s i)

Proof state:
case intro.intro
α : Type u_1
inst✝² : MeasurableSpace α
ι : Type u_6
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Monotone s
hs : ∃ᶠ (i : ι) in atTop, MeasurableSet (s i)
x : ℕ → ι
hx : Tendsto x atTop atTop
hxm : ∀ (n : ℕ), MeasurableSet (s (x n))
⊢ MeasurableSet (⋃ i, s i)

Tactic:
rw [← hsm.iUnion_comp_tendsto_atTop hx]

Result:
case intro.intro
α : Type u_1
inst✝² : MeasurableSpace α
ι : Type u_6
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Monotone s
hs : ∃ᶠ (i : ι) in atTop, MeasurableSet (s i)
x : ℕ → ι
hx : Tendsto x atTop atTop
hxm : ∀ (n : ℕ), MeasurableSet (s (x n))
⊢ MeasurableSet (⋃ a, s (x a))

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
ι : Type u_6
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Monotone s
hs : ∃ᶠ (i : ι) in atTop, MeasurableSet (s i)
⊢ MeasurableSet (⋃ i, s i)

Tactic:
rcases exists_seq_forall_of_frequently hs with ⟨x, hx, hxm⟩

Result:
case intro.intro
α : Type u_1
inst✝² : MeasurableSpace α
ι : Type u_6
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Monotone s
hs : ∃ᶠ (i : ι) in atTop, MeasurableSet (s i)
x : ℕ → ι
hx : Tendsto x atTop atTop
hxm : ∀ (n : ℕ), MeasurableSet (s (x n))
⊢ MeasurableSet (⋃ i, s i)

Proof state:
case intro.intro
α : Type u_1
inst✝² : MeasurableSpace α
ι : Type u_6
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Monotone s
hs : ∃ᶠ (i : ι) in atTop, MeasurableSet (s i)
x : ℕ → ι
hx : Tendsto x atTop atTop
hxm : ∀ (n : ℕ), MeasurableSet (s (x n))
⊢ MeasurableSet (⋃ a, s (x a))

Tactic:
exact .iUnion hxm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head?_map (f : α → β) (l : List α) : (map f l).head? = l.head?.map f

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ (map f l).head? = Option.map f l.head?

Tactic:
cases l <;> rfl

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem ofReal_tan_ofReal_re (x : ℝ) : ((tan x).re : ℂ) = tan x :=
  conj_eq_iff_re.1 <| by rw [← tan_conj, conj_ofReal]

Proof state:
x : ℝ
⊢ (starRingEnd ℂ) (tan ↑x) = tan ↑x

Tactic:
rw [← tan_conj, conj_ofReal]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem unit_aux (x : HahnSeries Γ R) {r : R} (hr : r * x.leadingCoeff = 1)
    (hxo : IsAddUnit x.order) : 0 < (1 - single (IsAddUnit.addUnit hxo).neg r * x).orderTop

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
r : R
hr : r * x.leadingCoeff = 1
hxo : IsAddUnit x.order
⊢ 0 < (1 - (single hxo.addUnit.neg) r * x).orderTop

Tactic:
let y := (x - single x.order x.leadingCoeff)

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
r : R
hr : r * x.leadingCoeff = 1
hxo : IsAddUnit x.order
y : HahnSeries Γ R := x - (single x.order) x.leadingCoeff
⊢ 0 < (1 - (single hxo.addUnit.neg) r * x).orderTop

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
r : R
hr : r * x.leadingCoeff = 1
hxo : IsAddUnit x.order
y : HahnSeries Γ R := x - (single x.order) x.leadingCoeff
hy : y = 0
⊢ (single hxo.addUnit.neg) r * x = 1

Tactic:
nth_rw 2 [eq_of_sub_eq_zero hy]

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
r : R
hr : r * x.leadingCoeff = 1
hxo : IsAddUnit x.order
y : HahnSeries Γ R := x - (single x.order) x.leadingCoeff
hy : y = 0
⊢ (single hxo.addUnit.neg) r * (single x.order) x.leadingCoeff = 1

Proof state:
case neg
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
r : R
hr : r * x.leadingCoeff = 1
hxo : IsAddUnit x.order
y : HahnSeries Γ R := x - (single x.order) x.leadingCoeff
hy : ¬y = 0
hr' : IsRegular r
hy' : 0 < ((single hxo.addUnit.neg) r * y).order
⊢ 0 < ((single hxo.addUnit.neg) r * (x - (single x.order) x.leadingCoeff)).orderTop

Tactic:
exact zero_lt_orderTop_of_order hy'

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem Sublist.lookup_isSome {l₁ l₂ : List (α × β)} (h : l₁ <+ l₂) :
    (l₁.lookup k).isSome → (l₂.lookup k).isSome

Proof state:
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
k : α
l₁ l₂ : List (α × β)
h : l₁ <+ l₂
⊢ (lookup k l₁).isSome = true → (lookup k l₂).isSome = true

Tactic:
simp only [lookup_eq_findSome?]

Result:
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
k : α
l₁ l₂ : List (α × β)
h : l₁ <+ l₂
⊢ (findSome? (fun p => if (k == p.fst) = true then some p.snd else none) l₁).isSome = true →
    (findSome? (fun p => if (k == p.fst) = true then some p.snd else none) l₂).isSome = true

Proof state:
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
k : α
l₁ l₂ : List (α × β)
h : l₁ <+ l₂
⊢ (findSome? (fun p => if (k == p.fst) = true then some p.snd else none) l₁).isSome = true →
    (findSome? (fun p => if (k == p.fst) = true then some p.snd else none) l₂).isSome = true

Tactic:
exact h.findSome?_isSome

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Pullback.lean
lemma pullbackShiftFunctorZero'_inv_app :
    (shiftFunctorZero _ A).inv.app X = (shiftFunctorZero' C (φ 0) (by rw [map_zero])).inv.app X ≫
      (pullbackShiftIso C φ 0 (φ 0) rfl).inv.app X

Proof state:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
⊢ (shiftFunctorZero C B).inv.app X ≫ eqToHom ⋯ =
    (shiftFunctorZero C B).inv.app X ≫ eqToHom ⋯ ≫ 𝟙 ((shiftFunctor (PullbackShift C φ) 0).obj X)

Tactic:
erw [comp_id]

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
⊢ (shiftFunctorZero (PullbackShift C φ) A).inv.app X =
    (shiftFunctorZero' C (φ 0) ⋯).inv.app X ≫ (pullbackShiftIso C φ 0 (φ 0) ⋯).inv.app X

Tactic:
rw [pullbackShiftFunctorZero_inv_app]

Result:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
⊢ (shiftFunctorZero C B).inv.app X ≫ (pullbackShiftIso C φ 0 0 ⋯).inv.app X =
    (shiftFunctorZero' C (φ 0) ⋯).inv.app X ≫ (pullbackShiftIso C φ 0 (φ 0) ⋯).inv.app X

Proof state:
C : Type u_1
inst✝³ : Category.{?u.13617, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
⊢ φ 0 = 0

Tactic:
rw [map_zero]

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
⊢ (shiftFunctorZero C B).inv.app X ≫ (pullbackShiftIso C φ 0 0 ⋯).inv.app X =
    (shiftFunctorZero' C (φ 0) ⋯).inv.app X ≫ (pullbackShiftIso C φ 0 (φ 0) ⋯).inv.app X

Tactic:
simp only [Functor.id_obj, pullbackShiftIso, eqToIso.inv, eqToHom_app, shiftFunctorZero',
  Iso.trans_inv, NatTrans.comp_app, eqToIso_refl, Iso.refl_inv, NatTrans.id_app, assoc]

Result:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
⊢ (shiftFunctorZero C B).inv.app X ≫ eqToHom ⋯ =
    (shiftFunctorZero C B).inv.app X ≫ eqToHom ⋯ ≫ 𝟙 ((shiftFunctor (PullbackShift C φ) 0).obj X)
-- Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean
lemma targetAffineLocally_affineAnd_iff (hQi : RingHom.RespectsIso Q)
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    targetAffineLocally (affineAnd Q) f ↔ ∀ U : Y.Opens, IsAffineOpen U →
      IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (f.app U).hom

Proof state:
case refine_1
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
f : X ⟶ Y
hf : ∀ (U : ↑Y.affineOpens), IsAffine ↑(f ⁻¹ᵁ ↑U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U).ι ''ᵁ ⊤)))
U : Y.Opens
hU : IsAffineOpen U
⊢ IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
obtain ⟨hfU, hf⟩ := hf ⟨U, hU⟩

Result:
case refine_1.intro
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
f : X ⟶ Y
hf✝ : ∀ (U : ↑Y.affineOpens), IsAffine ↑(f ⁻¹ᵁ ↑U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U).ι ''ᵁ ⊤)))
U : Y.Opens
hU : IsAffineOpen U
hfU : IsAffine ↑(f ⁻¹ᵁ ↑⟨U, hU⟩)
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑⟨U, hU⟩).ι ''ᵁ ⊤)))
⊢ IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
-- Mathlib/MeasureTheory/Constructions/Projective.lean
/-- Auxiliary lemma for `measure_univ_eq`. -/
lemma measure_univ_eq_of_subset (hP : IsProjectiveMeasureFamily P) (hJI : J ⊆ I) :
    P I univ = P J univ

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
hJI : J ⊆ I
this : univ = Finset.restrict₂ hJI ⁻¹' univ
⊢ (Measure.map (Finset.restrict₂ hJI) (P I)) univ = (P J) univ

Tactic:
rw [hP I J hJI]

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
hJI : J ⊆ I
⊢ univ = Finset.restrict₂ hJI ⁻¹' univ

Tactic:
rw [preimage_univ]

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
hJI : J ⊆ I
this : univ = Finset.restrict₂ hJI ⁻¹' univ
⊢ Measurable (Finset.restrict₂ hJI)

Tactic:
exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _)

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
hJI : J ⊆ I
⊢ (P I) univ = (P J) univ

Tactic:
have : (univ : Set (∀ i : I, α i)) =
    Finset.restrict₂ hJI ⁻¹' (univ : Set (∀ i : J, α i)) := by
  rw [preimage_univ]

Result:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
hJI : J ⊆ I
this : univ = Finset.restrict₂ hJI ⁻¹' univ
⊢ (P I) univ = (P J) univ

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
hJI : J ⊆ I
this : univ = Finset.restrict₂ hJI ⁻¹' univ
⊢ (P I) univ = (P J) univ

Tactic:
rw [this, ← Measure.map_apply _ MeasurableSet.univ]

Result:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
hJI : J ⊆ I
this : univ = Finset.restrict₂ hJI ⁻¹' univ
⊢ (Measure.map (Finset.restrict₂ hJI) (P I)) univ = (P J) univ

ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
hJI : J ⊆ I
this : univ = Finset.restrict₂ hJI ⁻¹' univ
⊢ MeasurableSpace ((i : { x // x ∈ J }) → α ↑i)

ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
hJI : J ⊆ I
this : univ = Finset.restrict₂ hJI ⁻¹' univ
⊢ Measurable (Finset.restrict₂ hJI)
-- Mathlib/Algebra/Group/Submonoid/BigOperators.lean
theorem multiset_prod_mem {M} [CommMonoid M] (S : Submonoid M) (m : Multiset M)
    (hm : ∀ a ∈ m, a ∈ S) : m.prod ∈ S

Proof state:
case intro
M : Type u_4
inst✝ : CommMonoid M
S : Submonoid M
m : Multiset ↥S
⊢ ↑m.prod ∈ S

Tactic:
exact m.prod.coe_prop

Result:
no goals

Proof state:
case intro
M : Type u_4
inst✝ : CommMonoid M
S : Submonoid M
m : Multiset ↥S
⊢ (Multiset.map Subtype.val m).prod ∈ S

Tactic:
rw [← coe_multiset_prod]

Result:
case intro
M : Type u_4
inst✝ : CommMonoid M
S : Submonoid M
m : Multiset ↥S
⊢ ↑m.prod ∈ S

Proof state:
M : Type u_4
inst✝ : CommMonoid M
S : Submonoid M
m : Multiset M
hm : ∀ a ∈ m, a ∈ S
⊢ m.prod ∈ S

Tactic:
lift m to Multiset S using hm

Result:
case intro
M : Type u_4
inst✝ : CommMonoid M
S : Submonoid M
m : Multiset ↥S
⊢ (Multiset.map Subtype.val m).prod ∈ S
-- Mathlib/Algebra/Ring/Ext.lean
theorem AddMonoidWithOne.ext ⦃inst₁ inst₂ : AddMonoidWithOne R⦄
    (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂])
    (h_one : (letI := inst₁; One.one : R) = (letI := inst₂; One.one : R)) :
    inst₁ = inst₂

Proof state:
case h.succ
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : toAddMonoid = toAddMonoid
h_zero' : AddMonoid.toZero = AddMonoid.toZero
h_one' : toOne = toOne
n : ℕ
h : NatCast.natCast n = NatCast.natCast n
⊢ NatCast.natCast n + 1 = NatCast.natCast n + 1

Tactic:
exact congrArg₂ _ h h_one

Result:
no goals

Proof state:
case h_mul
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
⊢ HAdd.hAdd = HAdd.hAdd

Tactic:
exact h_add

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Pairwise.lean
theorem getElem?_inj {xs : List α}
    (h₀ : i < xs.length) (h₁ : Nodup xs) (h₂ : xs[i]? = xs[j]?) : i = j

Proof state:
case cons.refine_1
α : Type u_1
x : α
xs : List α
ih : ∀ {i j : Nat}, i < xs.length → xs.Nodup → xs[i]? = xs[j]? → i = j
i✝ j : Nat
h₁ : (x :: xs).Nodup
i : Nat
h₀ : i + 1 < (x :: xs).length
h₂ : (x :: xs)[i + 1]? = (x :: xs)[0]?
⊢ i + 1 = 0

case cons.refine_2
α : Type u_1
x : α
xs : List α
ih : ∀ {i j : Nat}, i < xs.length → xs.Nodup → xs[i]? = xs[j]? → i = j
i j✝ : Nat
h₁ : (x :: xs).Nodup
j : Nat
h₀ : 0 < (x :: xs).length
h₂ : (x :: xs)[0]? = (x :: xs)[j + 1]?
⊢ 0 = j + 1

Tactic:
all_goals
  simp only [get?_eq_getElem?, getElem?_cons_zero, getElem?_cons_succ] at h₂
  cases h₁; rename_i h' h
  have := h x ?_ rfl; cases this
  rw [mem_iff_get?]
  simp only [get?_eq_getElem?]

Result:
case cons.refine_1.cons.refine_1
α : Type u_1
x : α
xs : List α
ih : ∀ {i j : Nat}, i < xs.length → xs.Nodup → xs[i]? = xs[j]? → i = j
i✝ j i : Nat
h₀ : i + 1 < (x :: xs).length
h₂ : xs[i]? = some x
h' : Pairwise (fun x1 x2 => x1 ≠ x2) xs
h : ∀ (a' : α), a' ∈ xs → x ≠ a'
⊢ ∃ n, xs[n]? = some x

case cons.refine_2.cons.refine_1
α : Type u_1
x : α
xs : List α
ih : ∀ {i j : Nat}, i < xs.length → xs.Nodup → xs[i]? = xs[j]? → i = j
i j✝ j : Nat
h₀ : 0 < (x :: xs).length
h₂ : some x = xs[j]?
h' : Pairwise (fun x1 x2 => x1 ≠ x2) xs
h : ∀ (a' : α), a' ∈ xs → x ≠ a'
⊢ ∃ n, xs[n]? = some x
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc (attr := simp)]
lemma LeftHomologyData.π_comp_homologyIso_inv (h : S.LeftHomologyData) :
    h.π ≫ h.homologyIso.inv = h.cyclesIso.inv ≫ S.homologyπ

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ h.π ≫ h.homologyIso.inv = h.cyclesIso.inv ≫ S.homologyπ

Tactic:
dsimp only [homologyπ, homologyIso]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ h.π ≫ (S.leftHomologyIso.symm ≪≫ h.leftHomologyIso).inv = h.cyclesIso.inv ≫ S.leftHomologyπ ≫ S.leftHomologyIso.hom

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ h.π ≫ (S.leftHomologyIso.symm ≪≫ h.leftHomologyIso).inv = h.cyclesIso.inv ≫ S.leftHomologyπ ≫ S.leftHomologyIso.hom

Tactic:
simp only [Iso.trans_inv, Iso.symm_inv, π_comp_leftHomologyIso_inv_assoc]

Result:
no goals
-- Mathlib/RingTheory/RingHom/Integral.lean
theorem isIntegral_respectsIso : RespectsIso fun f => f.IsIntegral

Proof state:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
x : S
⊢ e.toRingHom.IsIntegralElem x

Tactic:
rw [← e.apply_symm_apply x]

Result:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
x : S
⊢ e.toRingHom.IsIntegralElem (e (e.symm x))

Proof state:
⊢ RespectsIso fun {R S} [CommRing R] [CommRing S] f => f.IsIntegral

Tactic:
apply isIntegral_stableUnderComposition.respectsIso

Result:
⊢ ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.IsIntegral

Proof state:
⊢ ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.IsIntegral

Tactic:
introv x

Result:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
x : S
⊢ e.toRingHom.IsIntegralElem x

Proof state:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
x : S
⊢ e.toRingHom.IsIntegralElem (e (e.symm x))

Tactic:
apply RingHom.isIntegralElem_map

Result:
no goals
-- Mathlib/Analysis/Analytic/IsolatedZeros.lean
theorem exists_hasSum_smul_of_apply_eq_zero (hs : HasSum (fun m => z ^ m • a m) s)
    (ha : ∀ k < n, a k = 0) : ∃ t : E, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : z = 0
this : s = 0
⊢ HasSum (fun m => z ^ m • a (m + n)) (a n)

Tactic:
simpa [h] using hasSum_at_zero fun m => a (m + n)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
⊢ z ^ n • (z ^ n)⁻¹ • s = s

Tactic:
field_simp [smul_smul]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : z = 0
this : s = 0
⊢ z ^ n • a n = s

Tactic:
simp [h, hn.ne', this]

Result:
no goals

Proof state:
case h.e'_6
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
h1 : ∑ i ∈ Finset.range n, z ^ i • a i = 0
h2 : HasSum (fun m => z ^ (m + n) • a (m + n)) s
⊢ (z ^ n)⁻¹ • s = z⁻¹ ^ n • s

Tactic:
simp only [inv_pow]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
k : ℕ
hk : k ∈ Finset.range n
⊢ z ^ k • a k = 0

Tactic:
simp [ha k (Finset.mem_range.mp hk)]

Result:
no goals

Proof state:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : z = 0
this : s = 0
⊢ ∃ t, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t

Tactic:
exact ⟨a n, by simp [h, hn.ne', this], by simpa [h] using hasSum_at_zero fun m => a (m + n)⟩

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Removal.lean
lemma triangleRemovalBound_mul_cube_lt (hε : 0 < ε) :
    triangleRemovalBound ε * ⌈4 / ε⌉₊ ^ 3 < 1

Proof state:
case h
ε : ℝ
hε : 0 < ε
⊢ ↑⌈4 / ε⌉₊ ^ 3 ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
ε : ℝ
hε : 0 < ε
⊢ 2⁻¹ < 1

Tactic:
norm_num

Result:
no goals

Proof state:
ε : ℝ
hε : 0 < ε
⊢ triangleRemovalBound ε * ↑⌈4 / ε⌉₊ ^ 3 < 1

Tactic:
calc
  _ ≤ (2 * ⌈4 / ε⌉₊ ^ 3 : ℝ)⁻¹ * ↑⌈4 / ε⌉₊ ^ 3 := by gcongr; exact min_le_left _ _
  _ = 2⁻¹ := by rw [mul_inv, inv_mul_cancel_right₀]; positivity
  _ < 1 := by norm_num

Result:
no goals

Proof state:
case h
ε : ℝ
hε : 0 < ε
⊢ triangleRemovalBound ε ≤ (2 * ↑⌈4 / ε⌉₊ ^ 3)⁻¹

Tactic:
exact min_le_left _ _

Result:
no goals

Proof state:
ε : ℝ
hε : 0 < ε
⊢ triangleRemovalBound ε * ↑⌈4 / ε⌉₊ ^ 3 ≤ (2 * ↑⌈4 / ε⌉₊ ^ 3)⁻¹ * ↑⌈4 / ε⌉₊ ^ 3

Tactic:
gcongr

Result:
case h
ε : ℝ
hε : 0 < ε
⊢ triangleRemovalBound ε ≤ (2 * ↑⌈4 / ε⌉₊ ^ 3)⁻¹

Proof state:
ε : ℝ
hε : 0 < ε
⊢ (2 * ↑⌈4 / ε⌉₊ ^ 3)⁻¹ * ↑⌈4 / ε⌉₊ ^ 3 = 2⁻¹

Tactic:
rw [mul_inv, inv_mul_cancel_right₀]

Result:
case h
ε : ℝ
hε : 0 < ε
⊢ ↑⌈4 / ε⌉₊ ^ 3 ≠ 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem eraseIdx_set_gt {l : Array α} {i : Nat} {j : Nat} {a : α} (h : i < j) {w : j < l.size} :
    (l.set i a).eraseIdx j (by simp; omega) = (l.eraseIdx j).set i a (by simp; omega)

Proof state:
α : Type ?u.74309
l : Array α
i j : Nat
a : α
h : i < j
w : j < l.size
⊢ i < l.size - 1

Tactic:
omega

Result:
no goals

Proof state:
case mk
α : Type u_1
i j : Nat
a : α
h : i < j
l : List α
w : j < { toList := l }.size
⊢ ({ toList := l }.set i a ⋯).eraseIdx j ⋯ = ({ toList := l }.eraseIdx j w).set i a ⋯

Tactic:
simp [List.eraseIdx_set_gt, *]

Result:
no goals

Proof state:
α : Type ?u.74309
l : Array α
i j : Nat
a : α
h : i < j
w : j < l.size
⊢ i < (l.eraseIdx j w).size

Tactic:
simp

Result:
α : Type ?u.74309
l : Array α
i j : Nat
a : α
h : i < j
w : j < l.size
⊢ i < l.size - 1

Proof state:
α : Type u_1
l : Array α
i j : Nat
a : α
h : i < j
w : j < l.size
⊢ (l.set i a ⋯).eraseIdx j ⋯ = (l.eraseIdx j w).set i a ⋯

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
i j : Nat
a : α
h : i < j
l : List α
w : j < { toList := l }.size
⊢ ({ toList := l }.set i a ⋯).eraseIdx j ⋯ = ({ toList := l }.eraseIdx j w).set i a ⋯

Proof state:
α : Type ?u.74309
l : Array α
i j : Nat
a : α
h : i < j
w : j < l.size
⊢ j < (l.set i a ⋯).size

Tactic:
simp

Result:
α : Type ?u.74309
l : Array α
i j : Nat
a : α
h : i < j
w : j < l.size
⊢ j < l.size

Proof state:
α : Type ?u.74309
l : Array α
i j : Nat
a : α
h : i < j
w : j < l.size
⊢ j < l.size

Tactic:
omega

Result:
no goals