harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/ZFC/Rank.lean
theorem rank_lt_of_mem : ∀ {x y : PSet}, y ∈ x → rank y < rank x
  | ⟨_, _⟩, _, ⟨_, h⟩ => by
    rw [rank_congr h, ← succ_le_iff]
    apply Ordinal.le_iSup

Proof state:
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
x✝ : PSet.{u_1}
w✝ : (mk α✝ A✝).Type
h : x✝.Equiv ((mk α✝ A✝).Func w✝)
⊢ succ ((mk α✝ A✝).Func w✝).rank ≤ (mk α✝ A✝).rank

Tactic:
apply Ordinal.le_iSup

Result:
no goals

Proof state:
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
x✝ : PSet.{u_1}
w✝ : (mk α✝ A✝).Type
h : x✝.Equiv ((mk α✝ A✝).Func w✝)
⊢ x✝.rank < (mk α✝ A✝).rank

Tactic:
rw [rank_congr h, ← succ_le_iff]

Result:
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
x✝ : PSet.{u_1}
w✝ : (mk α✝ A✝).Type
h : x✝.Equiv ((mk α✝ A✝).Func w✝)
⊢ succ ((mk α✝ A✝).Func w✝).rank ≤ (mk α✝ A✝).rank
-- Mathlib/CategoryTheory/NatIso.lean
@[reassoc (attr := simp)]
lemma hom_inv_id_app_app_app {F G : C ⥤ D ⥤ E ⥤ E'} (e : F ≅ G)
    (X₁ : C) (X₂ : D) (X₃ : E) :
    ((e.hom.app X₁).app X₂).app X₃ ≫ ((e.inv.app X₁).app X₂).app X₃ = 𝟙 _

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F G : C ⥤ D ⥤ E ⥤ E'
e : F ≅ G
X₁ : C
X₂ : D
X₃ : E
⊢ ((e.hom.app X₁).app X₂).app X₃ ≫ ((e.inv.app X₁).app X₂).app X₃ = 𝟙 (((F.obj X₁).obj X₂).obj X₃)

Tactic:
rw [← NatTrans.comp_app, ← NatTrans.comp_app, Iso.hom_inv_id_app,
  NatTrans.id_app, NatTrans.id_app]

Result:
no goals
-- Mathlib/NumberTheory/Dioph.lean
theorem IsPoly.add {f g : (α → ℕ) → ℤ} (hf : IsPoly f) (hg : IsPoly g) : IsPoly (f + g)

Proof state:
α : Type u_1
f g : (α → ℕ) → ℤ
hf : IsPoly f
hg : IsPoly g
⊢ IsPoly (f - -g)

Tactic:
exact hf.sub hg.neg

Result:
no goals

Proof state:
α : Type u_1
f g : (α → ℕ) → ℤ
hf : IsPoly f
hg : IsPoly g
⊢ IsPoly (f + g)

Tactic:
rw [← sub_neg_eq_add]

Result:
α : Type u_1
f g : (α → ℕ) → ℤ
hf : IsPoly f
hg : IsPoly g
⊢ IsPoly (f - -g)
-- Mathlib/AlgebraicGeometry/SpreadingOut.lean
/--
A variant of `spread_out_unique_of_isGermInjective`
whose condition is an equality of scheme morphisms instead of ring homomorphisms.
-/
lemma spread_out_unique_of_isGermInjective' {x : X} [X.IsGermInjectiveAt x]
    (f g : X ⟶ Y)
    (e : X.fromSpecStalk x ≫ f = X.fromSpecStalk x ≫ g) :
    ∃ (U : X.Opens), x ∈ U ∧ U.ι ≫ f = U.ι ≫ g

Proof state:
case H.a
X Y : Scheme
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : X.fromSpecStalk x ≫ f = X.fromSpecStalk x ≫ g
⊢ Spec.map (Scheme.Hom.stalkMap f x) = Spec.map (Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x)

Tactic:
rw [← cancel_mono (Y.fromSpecStalk _)]

Result:
case H.a
X Y : Scheme
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : X.fromSpecStalk x ≫ f = X.fromSpecStalk x ≫ g
⊢ Spec.map (Scheme.Hom.stalkMap f x) ≫ Y.fromSpecStalk ((ConcreteCategory.hom f.base) x) =
    Spec.map (Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x) ≫
      Y.fromSpecStalk ((ConcreteCategory.hom f.base) x)

Proof state:
case H
X Y : Scheme
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : X.fromSpecStalk x ≫ f = X.fromSpecStalk x ≫ g
⊢ Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x

Tactic:
apply Spec.map_injective

Result:
case H.a
X Y : Scheme
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : X.fromSpecStalk x ≫ f = X.fromSpecStalk x ≫ g
⊢ Spec.map (Scheme.Hom.stalkMap f x) = Spec.map (Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x)

Proof state:
case H.a
X Y : Scheme
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : X.fromSpecStalk x ≫ f = X.fromSpecStalk x ≫ g
⊢ Spec.map (Scheme.Hom.stalkMap f x) ≫ Y.fromSpecStalk ((ConcreteCategory.hom f.base) x) =
    Spec.map (Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x) ≫
      Y.fromSpecStalk ((ConcreteCategory.hom f.base) x)

Tactic:
simpa [Scheme.Spec_map_stalkSpecializes_fromSpecStalk]

Result:
no goals

Proof state:
X Y : Scheme
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : X.fromSpecStalk x ≫ f = X.fromSpecStalk x ≫ g
⊢ ∃ U, x ∈ U ∧ U.ι ≫ f = U.ι ≫ g

Tactic:
fapply spread_out_unique_of_isGermInjective

Result:
case e
X Y : Scheme
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : X.fromSpecStalk x ≫ f = X.fromSpecStalk x ≫ g
⊢ (ConcreteCategory.hom f.base) x = (ConcreteCategory.hom g.base) x

case H
X Y : Scheme
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : X.fromSpecStalk x ≫ f = X.fromSpecStalk x ≫ g
⊢ Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x

Proof state:
case e
X Y : Scheme
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : X.fromSpecStalk x ≫ f = X.fromSpecStalk x ≫ g
⊢ (ConcreteCategory.hom f.base) x = (ConcreteCategory.hom g.base) x

Tactic:
simpa using congr(($e).base (IsLocalRing.closedPoint _))

Result:
no goals
-- Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean
@[ext]
lemma SecondObj.ext (z₁ z₂ : SecondObj P X π) (h : ∀ ij, (Pi.π _ ij : SecondObj P X π ⟶ _) z₁ =
    (Pi.π _ ij : SecondObj P X π ⟶ _) z₂) : z₁ = z₂

Proof state:
case w.mk
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).hasPullbacks
z₁ z₂ : SecondObj P X π
h :
  ∀ (ij : I × I),
    Pi.π (fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij z₁ =
      Pi.π (fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij z₂
i : I × I
⊢ limit.π (Discrete.functor fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) { as := i } z₁ =
    limit.π (Discrete.functor fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) { as := i } z₂

Tactic:
exact h i

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).hasPullbacks
z₁ z₂ : SecondObj P X π
h :
  ∀ (ij : I × I),
    Pi.π (fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij z₁ =
      Pi.π (fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij z₂
⊢ z₁ = z₂

Tactic:
apply Limits.Types.limit_ext

Result:
case w
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).hasPullbacks
z₁ z₂ : SecondObj P X π
h :
  ∀ (ij : I × I),
    Pi.π (fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij z₁ =
      Pi.π (fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij z₂
⊢ ∀ (j : Discrete (I × I)),
    limit.π (Discrete.functor fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) j z₁ =
      limit.π (Discrete.functor fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) j z₂

Proof state:
case w
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).hasPullbacks
z₁ z₂ : SecondObj P X π
h :
  ∀ (ij : I × I),
    Pi.π (fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij z₁ =
      Pi.π (fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij z₂
⊢ ∀ (j : Discrete (I × I)),
    limit.π (Discrete.functor fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) j z₁ =
      limit.π (Discrete.functor fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) j z₂

Tactic:
rintro ⟨i⟩

Result:
case w.mk
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).hasPullbacks
z₁ z₂ : SecondObj P X π
h :
  ∀ (ij : I × I),
    Pi.π (fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij z₁ =
      Pi.π (fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij z₂
i : I × I
⊢ limit.π (Discrete.functor fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) { as := i } z₁ =
    limit.π (Discrete.functor fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) { as := i } z₂
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lcm.lean
theorem lcm_one_right (m : Nat) : lcm m 1 = m

Proof state:
m : Nat
⊢ m.lcm 1 = m

Tactic:
simp [lcm]

Result:
no goals
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
lemma conductor_le_conductor_mem_conductorSet {d : ℕ} (hd : d ∈ conductorSet χ) :
    χ.conductor ≤ (Classical.choose hd.2).conductor

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
hd : d ∈ χ.conductorSet
⊢ χ = (changeLevel ⋯) ⋯.choose

Tactic:
rw [changeLevel_trans _ (conductor_dvd_level _) hd.dvd,
    ← (factorsThrough_conductor (Classical.choose hd.2)).2.choose_spec]

Result:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
hd : d ∈ χ.conductorSet
⊢ χ = (changeLevel ⋯) (Classical.choose ⋯)

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
hd : d ∈ χ.conductorSet
⊢ χ.conductor ≤ (Classical.choose ⋯).conductor

Tactic:
refine Nat.sInf_le <| (mem_conductorSet_iff χ).mpr <|
  ⟨dvd_trans (conductor_dvd_level _) hd.1,
   (factorsThrough_conductor (Classical.choose hd.2)).2.choose, ?_⟩

Result:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
hd : d ∈ χ.conductorSet
⊢ χ = (changeLevel ⋯) ⋯.choose

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
hd : d ∈ χ.conductorSet
⊢ χ = (changeLevel ⋯) (Classical.choose ⋯)

Tactic:
exact hd.eq_changeLevel

Result:
no goals
-- Mathlib/Probability/Independence/ZeroOne.lean
theorem Kernel.indep_limsup_atBot_self (h_le : ∀ n, s n ≤ m0) (h_indep : iIndep s κ μα) :
    Indep (limsup s atBot) (limsup s atBot) κ μα

Proof state:
case refine_3
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ ∀ (n : ι), ∃ a, n ∈ ns a

Tactic:
exact fun n => ⟨n, le_rfl⟩

Result:
no goals

Proof state:
case refine_1.intro.intro
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}
b : ι
hb : b < a
c : ι
hc : c ≤ b
hct : c ∈ t
⊢ False

Tactic:
suffices ∀ i ∈ t, c < i from lt_irrefl c (this c hct)

Result:
case refine_1.intro.intro
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}
b : ι
hb : b < a
c : ι
hc : c ≤ b
hct : c ∈ t
⊢ ∀ i ∈ t, c < i
-- Mathlib/MeasureTheory/OuterMeasure/Operations.lean
theorem map_le_restrict_range {β} {ma : OuterMeasure α} {mb : OuterMeasure β} {f : α → β} :
    map f ma ≤ restrict (range f) mb ↔ map f ma ≤ mb :=
  ⟨fun h => h.trans (restrict_le_self _ _), fun h s => by simpa using h (s ∩ range f)⟩

Proof state:
α : Type u_1
β : Type u_3
ma : OuterMeasure α
mb : OuterMeasure β
f : α → β
h : (map f) ma ≤ mb
s : Set β
⊢ ((map f) ma) s ≤ ((restrict (range f)) mb) s

Tactic:
simpa using h (s ∩ range f)

Result:
no goals
-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem IsUniversalColimit.of_iso {F : J ⥤ C} {c c' : Cocone F} (hc : IsUniversalColimit c)
    (e : c ≅ c') : IsUniversalColimit c'

Proof state:
J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
this : c'.ι ≫ (Functor.const J).map e.inv.hom = c.ι
⊢ α ≫ c.ι = c''.ι ≫ (Functor.const J).map (f ≫ e.inv.hom)

Tactic:
rw [Functor.map_comp, ← reassoc_of% h, this]

Result:
no goals

Proof state:
J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
this✝ : c'.ι ≫ (Functor.const J).map e.inv.hom = c.ι
j : J
this : IsIso e.inv.hom
⊢ IsPullback (c''.ι.app j) (α.app j ≫ 𝟙 (F.obj j)) (f ≫ e.inv.hom) (c.ι.app j)

Tactic:
exact (H j).paste_vert (IsPullback.of_vert_isIso ⟨by simp⟩)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem getElem?_zip_eq_some {l₁ : Vector α n} {l₂ : Vector β n} {z : α × β} {i : Nat} :
    (zip l₁ l₂)[i]? = some z ↔ l₁[i]? = some z.1 ∧ l₂[i]? = some z.2

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
z : α × β
i : Nat
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
⊢ ({ toArray := l₁, size_toArray := ⋯ }.zip { toArray := l₂, size_toArray := h })[i]? = some z ↔
    { toArray := l₁, size_toArray := ⋯ }[i]? = some z.fst ∧ { toArray := l₂, size_toArray := h }[i]? = some z.snd

Tactic:
simp [Array.getElem?_zip_eq_some]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l₁ : Vector α n
l₂ : Vector β n
z : α × β
i : Nat
⊢ (l₁.zip l₂)[i]? = some z ↔ l₁[i]? = some z.fst ∧ l₂[i]? = some z.snd

Tactic:
rcases l₁ with ⟨l₁, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
z : α × β
i : Nat
l₁ : Array α
l₂ : Vector β l₁.size
⊢ ({ toArray := l₁, size_toArray := ⋯ }.zip l₂)[i]? = some z ↔
    { toArray := l₁, size_toArray := ⋯ }[i]? = some z.fst ∧ l₂[i]? = some z.snd

Proof state:
case mk
α : Type u_1
β : Type u_2
z : α × β
i : Nat
l₁ : Array α
l₂ : Vector β l₁.size
⊢ ({ toArray := l₁, size_toArray := ⋯ }.zip l₂)[i]? = some z ↔
    { toArray := l₁, size_toArray := ⋯ }[i]? = some z.fst ∧ l₂[i]? = some z.snd

Tactic:
rcases l₂ with ⟨l₂, h⟩

Result:
case mk.mk
α : Type u_1
β : Type u_2
z : α × β
i : Nat
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
⊢ ({ toArray := l₁, size_toArray := ⋯ }.zip { toArray := l₂, size_toArray := h })[i]? = some z ↔
    { toArray := l₁, size_toArray := ⋯ }[i]? = some z.fst ∧ { toArray := l₂, size_toArray := h }[i]? = some z.snd
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem eq_σ_of_epi {n : ℕ} (θ : mk (n + 1) ⟶ mk n) [Epi θ] : ∃ i : Fin (n + 1), θ = σ i

Proof state:
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst✝ : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
⊢ Epi θ

Tactic:
infer_instance

Result:
no goals

Proof state:
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst✝ : Epi θ
⊢ ¬Function.Injective ⇑(Hom.toOrderHom θ)

Tactic:
by_contra h

Result:
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst✝ : Epi θ
h : Function.Injective ⇑(Hom.toOrderHom θ)
⊢ False

Proof state:
case intro.intro
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst✝ : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
⊢ ∃ i, θ = σ i

Tactic:
use i

Result:
case h
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst✝ : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
⊢ θ = σ i

Proof state:
case h
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst✝ : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
this : Epi (σ i ≫ θ')
⊢ θ = σ i

Tactic:
haveI := CategoryTheory.epi_of_epi (σ i) θ'

Result:
case h
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst✝ : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
this✝ : Epi (σ i ≫ θ')
this : Epi θ'
⊢ θ = σ i

Proof state:
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst✝ : Epi θ
⊢ ∃ i, θ = σ i

Tactic:
rcases eq_σ_comp_of_not_injective θ (by
  by_contra h
  simpa using le_of_mono (mono_iff_injective.mpr h)) with ⟨i, θ', h⟩

Result:
case intro.intro
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst✝ : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
⊢ ∃ i, θ = σ i

Proof state:
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst✝ : Epi θ
h : Function.Injective ⇑(Hom.toOrderHom θ)
⊢ False

Tactic:
simpa using le_of_mono (mono_iff_injective.mpr h)

Result:
no goals

Proof state:
case h
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst✝ : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
⊢ θ = σ i

Tactic:
haveI : Epi (σ i ≫ θ') := by
  rw [← h]
  infer_instance

Result:
case h
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst✝ : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
this : Epi (σ i ≫ θ')
⊢ θ = σ i

Proof state:
case h
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst✝ : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
this✝ : Epi (σ i ≫ θ')
this : Epi θ'
⊢ θ = σ i

Tactic:
rw [h, eq_id_of_epi θ', Category.comp_id]

Result:
no goals

Proof state:
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst✝ : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
⊢ Epi (σ i ≫ θ')

Tactic:
rw [← h]

Result:
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst✝ : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
⊢ Epi θ
-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
/-- The L-series of a Dirichlet character does not vanish on the right half-plane `re s > 1`. -/
lemma LSeries_ne_zero_of_one_lt_re {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) :
    L ↗χ s ≠ 0 :=
  fun h ↦ by simpa [h] using LSeries.mul_mu_eq_one χ hs

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
h : L (fun n => χ ↑n) s = 0
⊢ False

Tactic:
simpa [h] using LSeries.mul_mu_eq_one χ hs

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
theorem nontrivial_iff_exists_ne_one (S : Submonoid M) : Nontrivial S ↔ ∃ x ∈ S, x ≠ (1 : M) :=
  calc
    Nontrivial S ↔ ∃ x : S, x ≠ 1 := nontrivial_iff_exists_ne 1
    _ ↔ ∃ (x : _) (hx : x ∈ S), (⟨x, hx⟩ : S) ≠ ⟨1, S.one_mem⟩ := Subtype.exists
    _ ↔ ∃ x ∈ S, x ≠ (1 : M)

Proof state:
M : Type u_1
inst✝ : MulOneClass M
S : Submonoid M
⊢ (∃ x, ∃ (hx : x ∈ S), ⟨x, hx⟩ ≠ ⟨1, ⋯⟩) ↔ ∃ x ∈ S, x ≠ 1

Tactic:
simp [Ne]

Result:
no goals
-- Mathlib/Computability/TMToPartrec.lean
theorem unrev_ok {q s} {S : K' → List Γ'} :
    Reaches₁ (TM2.step tr) ⟨some (unrev q), s, S⟩
      ⟨some q, none, update (update S rev []) main (List.reverseAux (S rev) (S main))⟩ :=
  move_ok (by decide) <| splitAtPred_false _

Proof state:
q : Λ'
s : Option Γ'
S : K' → List Γ'
⊢ rev ≠ main

Tactic:
decide

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem eq_iSup_nat (m : Set X → ℝ≥0∞) : mkMetric' m = ⨆ n : ℕ, mkMetric'.pre m n⁻¹

Proof state:
case h
X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ (mkMetric' m) s = ⨆ i, (pre m (↑i)⁻¹) s

Tactic:
refine tendsto_nhds_unique (mkMetric'.tendsto_pre_nat m s)
  (tendsto_atTop_iSup fun k l hkl => mkMetric'.mono_pre_nat m hkl s)

Result:
no goals

Proof state:
case h
X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ (mkMetric' m) s = (⨆ n, pre m (↑n)⁻¹) s

Tactic:
rw [iSup_apply]

Result:
case h
X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ (mkMetric' m) s = ⨆ i, (pre m (↑i)⁻¹) s

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
⊢ mkMetric' m = ⨆ n, pre m (↑n)⁻¹

Tactic:
ext1 s

Result:
case h
X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ (mkMetric' m) s = (⨆ n, pre m (↑n)⁻¹) s
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
theorem map_piecewise_smul [DecidableEq ι] (c : ι → R) (m : ∀ i, M₁ i) (s : Finset ι) :
    f (s.piecewise (fun i => c i • m i) m) = (∏ i ∈ s, c i) • f m

Proof state:
case h
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
c : ι → R
m : (i : ι) → M₁ i
s✝ : Finset ι
j : ι
s : Finset ι
j_not_mem_s : j ∉ s
Hrec : f (s.piecewise (fun i => c i • m i) m) = (∏ i ∈ s, c i) • f m
i : ι
⊢ update (s.piecewise (fun i => c i • m i) m) j (m j) i = s.piecewise (fun i => c i • m i) m i

Tactic:
by_cases h : i = j

Result:
case pos
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
c : ι → R
m : (i : ι) → M₁ i
s✝ : Finset ι
j : ι
s : Finset ι
j_not_mem_s : j ∉ s
Hrec : f (s.piecewise (fun i => c i • m i) m) = (∏ i ∈ s, c i) • f m
i : ι
h : i = j
⊢ update (s.piecewise (fun i => c i • m i) m) j (m j) i = s.piecewise (fun i => c i • m i) m i

case neg
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
c : ι → R
m : (i : ι) → M₁ i
s✝ : Finset ι
j : ι
s : Finset ι
j_not_mem_s : j ∉ s
Hrec : f (s.piecewise (fun i => c i • m i) m) = (∏ i ∈ s, c i) • f m
i : ι
h : ¬i = j
⊢ update (s.piecewise (fun i => c i • m i) m) j (m j) i = s.piecewise (fun i => c i • m i) m i
-- Mathlib/Data/Fintype/Sum.lean
theorem Fintype.card_subtype_or_disjoint (p q : α → Prop) (h : Disjoint p q) [Fintype { x // p x }]
    [Fintype { x // q x }] [Fintype { x // p x ∨ q x }] :
    Fintype.card { x // p x ∨ q x } = Fintype.card { x // p x } + Fintype.card { x // q x }

Proof state:
case h.e'_3
α : Type u_1
p q : α → Prop
h : Disjoint p q
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x } + card { x // q x } = card ({ x // p x } ⊕ { x // q x })

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p q : α → Prop
h : Disjoint p q
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x ∨ q x } = card { x // p x } + card { x // q x }

Tactic:
classical
  convert Fintype.card_congr (subtypeOrEquiv p q h)
  simp

Result:
no goals

Proof state:
α : Type u_1
p q : α → Prop
h : Disjoint p q
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x ∨ q x } = card { x // p x } + card { x // q x }

Tactic:
convert Fintype.card_congr (subtypeOrEquiv p q h)

Result:
case h.e'_3
α : Type u_1
p q : α → Prop
h : Disjoint p q
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x } + card { x // q x } = card ({ x // p x } ⊕ { x // q x })
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma genEigenspace_top (f : End R M) (μ : R) :
    f.genEigenspace μ ⊤ = ⨆ k : ℕ, f.genEigenspace μ k

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
⊢ (f.genEigenspace μ) ⊤ = ⨆ k, (f.genEigenspace μ) ↑k

Tactic:
rw [genEigenspace_eq_iSup_genEigenspace_nat, iSup_subtype]

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
⊢ ⨆ i, ⨆ (h : ↑i ≤ ⊤), (f.genEigenspace μ) ↑↑⟨i, h⟩ = ⨆ k, (f.genEigenspace μ) ↑k

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
⊢ ⨆ i, ⨆ (h : ↑i ≤ ⊤), (f.genEigenspace μ) ↑↑⟨i, h⟩ = ⨆ k, (f.genEigenspace μ) ↑k

Tactic:
simp only [le_top, iSup_pos, OrderHom.coe_mk]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem add_emod_self {a b : Int} : (a + b) % b = a % b

Proof state:
a b : Int
⊢ (a + b) % b = a % b

Tactic:
have := add_mul_emod_self_left a b 1

Result:
a b : Int
this : (a + b * 1) % b = a % b
⊢ (a + b) % b = a % b

Proof state:
a b : Int
this : (a + b * 1) % b = a % b
⊢ (a + b) % b = a % b

Tactic:
rwa [Int.mul_one] at this

Result:
no goals