harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Functor/EpiMono.lean
theorem isSplitEpi_iff [Full F] [Faithful F] : IsSplitEpi (F.map f) ↔ IsSplitEpi f

Proof state:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ IsSplitEpi (F.map f) → IsSplitEpi f

Tactic:
intro h

Result:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
h : IsSplitEpi (F.map f)
⊢ IsSplitEpi f

Proof state:
case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ IsSplitEpi f → IsSplitEpi (F.map f)

Tactic:
intro h

Result:
case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
h : IsSplitEpi f
⊢ IsSplitEpi (F.map f)

Proof state:
case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
h : IsSplitEpi f
⊢ IsSplitEpi (F.map f)

Tactic:
exact IsSplitEpi.mk' ((splitEpiEquiv F f).toFun h.exists_splitEpi.some)

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ IsSplitEpi (F.map f) ↔ IsSplitEpi f

Tactic:
constructor

Result:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ IsSplitEpi (F.map f) → IsSplitEpi f

case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ IsSplitEpi f → IsSplitEpi (F.map f)

Proof state:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
h : IsSplitEpi (F.map f)
⊢ IsSplitEpi f

Tactic:
exact IsSplitEpi.mk' ((splitEpiEquiv F f).invFun h.exists_splitEpi.some)

Result:
no goals
-- Mathlib/CategoryTheory/Idempotents/Karoubi.lean
theorem ext {P Q : Karoubi C} (h_X : P.X = Q.X) (h_p : P.p ≫ eqToHom h_X = eqToHom h_X ≫ Q.p) :
    P = Q

Proof state:
case mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Q : Karoubi C
X✝ : C
p✝ : X✝ ⟶ X✝
idem✝ : p✝ ≫ p✝ = p✝
h_X : { X := X✝, p := p✝, idem := idem✝ }.X = Q.X
h_p : { X := X✝, p := p✝, idem := idem✝ }.p ≫ eqToHom h_X = eqToHom h_X ≫ Q.p
⊢ { X := X✝, p := p✝, idem := idem✝ } = Q

Tactic:
cases Q

Result:
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X✝¹ : C
p✝¹ : X✝¹ ⟶ X✝¹
idem✝¹ : p✝¹ ≫ p✝¹ = p✝¹
X✝ : C
p✝ : X✝ ⟶ X✝
idem✝ : p✝ ≫ p✝ = p✝
h_X : { X := X✝¹, p := p✝¹, idem := idem✝¹ }.X = { X := X✝, p := p✝, idem := idem✝ }.X
h_p : { X := X✝¹, p := p✝¹, idem := idem✝¹ }.p ≫ eqToHom h_X = eqToHom h_X ≫ { X := X✝, p := p✝, idem := idem✝ }.p
⊢ { X := X✝¹, p := p✝¹, idem := idem✝¹ } = { X := X✝, p := p✝, idem := idem✝ }

Proof state:
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X✝¹ : C
p✝¹ : X✝¹ ⟶ X✝¹
idem✝¹ : p✝¹ ≫ p✝¹ = p✝¹
X✝ : C
p✝ : X✝ ⟶ X✝
idem✝ : p✝ ≫ p✝ = p✝
h_X : { X := X✝¹, p := p✝¹, idem := idem✝¹ }.X = { X := X✝, p := p✝, idem := idem✝ }.X
h_p : { X := X✝¹, p := p✝¹, idem := idem✝¹ }.p ≫ eqToHom h_X = eqToHom h_X ≫ { X := X✝, p := p✝, idem := idem✝ }.p
⊢ { X := X✝¹, p := p✝¹, idem := idem✝¹ } = { X := X✝, p := p✝, idem := idem✝ }

Tactic:
dsimp at h_X h_p

Result:
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X✝¹ : C
p✝¹ : X✝¹ ⟶ X✝¹
idem✝¹ : p✝¹ ≫ p✝¹ = p✝¹
X✝ : C
p✝ : X✝ ⟶ X✝
idem✝ : p✝ ≫ p✝ = p✝
h_X : X✝¹ = X✝
h_p : p✝¹ ≫ eqToHom h_X = eqToHom h_X ≫ p✝
⊢ { X := X✝¹, p := p✝¹, idem := idem✝¹ } = { X := X✝, p := p✝, idem := idem✝ }

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
h_X : P.X = Q.X
h_p : P.p ≫ eqToHom h_X = eqToHom h_X ≫ Q.p
⊢ P = Q

Tactic:
cases P

Result:
case mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Q : Karoubi C
X✝ : C
p✝ : X✝ ⟶ X✝
idem✝ : p✝ ≫ p✝ = p✝
h_X : { X := X✝, p := p✝, idem := idem✝ }.X = Q.X
h_p : { X := X✝, p := p✝, idem := idem✝ }.p ≫ eqToHom h_X = eqToHom h_X ≫ Q.p
⊢ { X := X✝, p := p✝, idem := idem✝ } = Q

Proof state:
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X✝ : C
p✝¹ : X✝ ⟶ X✝
idem✝¹ : p✝¹ ≫ p✝¹ = p✝¹
p✝ : X✝ ⟶ X✝
idem✝ : p✝ ≫ p✝ = p✝
h_p : p✝¹ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ p✝
⊢ { X := X✝, p := p✝¹, idem := idem✝¹ } = { X := X✝, p := p✝, idem := idem✝ }

Tactic:
simpa only [mk.injEq, heq_eq_eq, true_and, eqToHom_refl, comp_id, id_comp] using h_p

Result:
no goals

Proof state:
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X✝¹ : C
p✝¹ : X✝¹ ⟶ X✝¹
idem✝¹ : p✝¹ ≫ p✝¹ = p✝¹
X✝ : C
p✝ : X✝ ⟶ X✝
idem✝ : p✝ ≫ p✝ = p✝
h_X : X✝¹ = X✝
h_p : p✝¹ ≫ eqToHom h_X = eqToHom h_X ≫ p✝
⊢ { X := X✝¹, p := p✝¹, idem := idem✝¹ } = { X := X✝, p := p✝, idem := idem✝ }

Tactic:
subst h_X

Result:
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X✝ : C
p✝¹ : X✝ ⟶ X✝
idem✝¹ : p✝¹ ≫ p✝¹ = p✝¹
p✝ : X✝ ⟶ X✝
idem✝ : p✝ ≫ p✝ = p✝
h_p : p✝¹ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ p✝
⊢ { X := X✝, p := p✝¹, idem := idem✝¹ } = { X := X✝, p := p✝, idem := idem✝ }
-- Mathlib/Data/List/Sigma.lean
theorem kreplace_of_forall_not (a : α) (b : β a) {l : List (Sigma β)}
    (H : ∀ b : β a, Sigma.mk a b ∉ l) : kreplace a b l = l :=
  lookmap_of_forall_not _ <| by
    rintro ⟨a', b'⟩ h; dsimp; split_ifs
    · subst a'
      exact H _ h
    · rfl

Proof state:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
H : ∀ (b : β a), ⟨a, b⟩ ∉ l
a' : α
b' : β a'
h : ⟨a', b'⟩ ∈ l
h✝ : ¬a = a'
⊢ none = none

Tactic:
rfl

Result:
no goals

Proof state:
case mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
H : ∀ (b : β a), ⟨a, b⟩ ∉ l
a' : α
b' : β a'
h : ⟨a', b'⟩ ∈ l
⊢ (if a = ⟨a', b'⟩.fst then some ⟨a, b⟩ else none) = none

Tactic:
dsimp

Result:
case mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
H : ∀ (b : β a), ⟨a, b⟩ ∉ l
a' : α
b' : β a'
h : ⟨a', b'⟩ ∈ l
⊢ (if a = a' then some ⟨a, b⟩ else none) = none

Proof state:
case mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
H : ∀ (b : β a), ⟨a, b⟩ ∉ l
a' : α
b' : β a'
h : ⟨a', b'⟩ ∈ l
⊢ (if a = a' then some ⟨a, b⟩ else none) = none

Tactic:
split_ifs

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
H : ∀ (b : β a), ⟨a, b⟩ ∉ l
a' : α
b' : β a'
h : ⟨a', b'⟩ ∈ l
h✝ : a = a'
⊢ False

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
H : ∀ (b : β a), ⟨a, b⟩ ∉ l
a' : α
b' : β a'
h : ⟨a', b'⟩ ∈ l
h✝ : ¬a = a'
⊢ none = none

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
H : ∀ (b : β a), ⟨a, b⟩ ∉ l
a' : α
b' : β a'
h : ⟨a', b'⟩ ∈ l
h✝ : a = a'
⊢ False

Tactic:
subst a'

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
H : ∀ (b : β a), ⟨a, b⟩ ∉ l
b' : β a
h : ⟨a, b'⟩ ∈ l
⊢ False

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
H : ∀ (b : β a), ⟨a, b⟩ ∉ l
b' : β a
h : ⟨a, b'⟩ ∈ l
⊢ False

Tactic:
exact H _ h

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
H : ∀ (b : β a), ⟨a, b⟩ ∉ l
⊢ ∀ a_1 ∈ l, (if a = a_1.fst then some ⟨a, b⟩ else none) = none

Tactic:
rintro ⟨a', b'⟩ h

Result:
case mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
H : ∀ (b : β a), ⟨a, b⟩ ∉ l
a' : α
b' : β a'
h : ⟨a', b'⟩ ∈ l
⊢ (if a = ⟨a', b'⟩.fst then some ⟨a, b⟩ else none) = none
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast_filterMap_of_eq_some {f : α → Option β} {l : List α} {w : l ≠ []} {b : β} (h : f (l.getLast w) = some b) :
    (filterMap f l).getLast (ne_nil_of_mem (mem_filterMap.2 ⟨_, getLast_mem w, h⟩)) = b

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
w : l ≠ []
b : β
h : f (l.getLast w) = some b
⊢ l.reverse ≠ []

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
w : l ≠ []
b : β
h : f (l.getLast w) = some b
⊢ f (l.reverse.head ⋯) = some b

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
w : l ≠ []
b : β
h : f (l.getLast w) = some b
⊢ (filterMap f l.reverse).head ⋯ = b

Tactic:
rw [head_filterMap_of_eq_some (by simp_all)]

Result:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
w : l ≠ []
b : β
h : f (l.getLast w) = some b
⊢ f (l.reverse.head ⋯) = some b

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
w : l ≠ []
b : β
h : f (l.getLast w) = some b
⊢ (filterMap f l).getLast ⋯ = b

Tactic:
simp only [getLast_eq_head_reverse, ← filterMap_reverse]

Result:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
w : l ≠ []
b : β
h : f (l.getLast w) = some b
⊢ (filterMap f l.reverse).head ⋯ = b
-- Mathlib/RingTheory/Generators.lean
lemma toAlgHom_ofComp_surjective (Q : Generators S T) (P : Generators R S) :
    Function.Surjective (Q.ofComp P).toAlgHom

Proof state:
case h_add.intro
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
q : MvPolynomial Q.vars S
hq : ∃ a, (Q.ofComp P).toAlgHom a = q
p : (Q.comp P).Ring
⊢ ∃ a, (Q.ofComp P).toAlgHom a = (Q.ofComp P).toAlgHom p + q

Tactic:
obtain ⟨q, rfl⟩ := hq

Result:
case h_add.intro.intro
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
p q : (Q.comp P).Ring
⊢ ∃ a, (Q.ofComp P).toAlgHom a = (Q.ofComp P).toAlgHom p + (Q.ofComp P).toAlgHom q

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
⊢ Function.Surjective ⇑(Q.ofComp P).toAlgHom

Tactic:
intro p

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
p : Q.Ring
⊢ ∃ a, (Q.ofComp P).toAlgHom a = p
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/String/Basic.lean
theorem lt_next (s : Substring) (i : String.Pos) (h : i.1 < s.bsize) :
    i.1 < (s.next i).1

Proof state:
case h
s : Substring
i : String.Pos
h : i.byteIdx < s.bsize
⊢ i.byteIdx + s.startPos.byteIdx < (s.str.next (s.startPos + i)).byteIdx

Tactic:
rw [Nat.add_comm]

Result:
case h
s : Substring
i : String.Pos
h : i.byteIdx < s.bsize
⊢ s.startPos.byteIdx + i.byteIdx < (s.str.next (s.startPos + i)).byteIdx

Proof state:
case h
s : Substring
i : String.Pos
h : i.byteIdx < s.bsize
⊢ s.startPos.byteIdx + i.byteIdx < (s.str.next (s.startPos + i)).byteIdx

Tactic:
apply String.lt_next

Result:
no goals

Proof state:
s : Substring
i : String.Pos
h : i.byteIdx < s.bsize
⊢ i.byteIdx <
    (ite (s.startPos + i = s.stopPos) i
        { byteIdx := (s.str.next (s.startPos + i)).byteIdx - s.startPos.byteIdx }).byteIdx

Tactic:
rw [if_neg ?a]

Result:
s : Substring
i : String.Pos
h : i.byteIdx < s.bsize
⊢ i.byteIdx < { byteIdx := (s.str.next (s.startPos + i)).byteIdx - s.startPos.byteIdx }.byteIdx

case a
s : Substring
i : String.Pos
h : i.byteIdx < s.bsize
⊢ ¬s.startPos + i = s.stopPos

Proof state:
s : Substring
i : String.Pos
h : i.byteIdx < s.bsize
⊢ ¬s.startPos + i = s.stopPos

Tactic:
refine mt (congrArg String.Pos.byteIdx) (Nat.ne_of_lt ?_)

Result:
s : Substring
i : String.Pos
h : i.byteIdx < s.bsize
⊢ (s.startPos + i).byteIdx < s.stopPos.byteIdx

Proof state:
s : Substring
i : String.Pos
h : i.byteIdx < s.bsize
⊢ i.byteIdx < { byteIdx := (s.str.next (s.startPos + i)).byteIdx - s.startPos.byteIdx }.byteIdx

Tactic:
apply Nat.lt_sub_of_add_lt

Result:
case h
s : Substring
i : String.Pos
h : i.byteIdx < s.bsize
⊢ i.byteIdx + s.startPos.byteIdx < (s.str.next (s.startPos + i)).byteIdx

Proof state:
s : Substring
i : String.Pos
h : i.byteIdx < s.bsize
⊢ (s.startPos + i).byteIdx < s.stopPos.byteIdx

Tactic:
exact (Nat.add_comm .. ▸ Nat.add_lt_of_lt_sub h :)

Result:
no goals

Proof state:
s : Substring
i : String.Pos
h : i.byteIdx < s.bsize
⊢ i.byteIdx < (s.next i).byteIdx

Tactic:
simp [next]

Result:
s : Substring
i : String.Pos
h : i.byteIdx < s.bsize
⊢ i.byteIdx <
    (ite (s.startPos + i = s.stopPos) i
        { byteIdx := (s.str.next (s.startPos + i)).byteIdx - s.startPos.byteIdx }).byteIdx

Proof state:
s : Substring
i : String.Pos
h : i.byteIdx < s.bsize
⊢ i.byteIdx < { byteIdx := (s.str.next (s.startPos + i)).byteIdx - s.startPos.byteIdx }.byteIdx

case a
s : Substring
i : String.Pos
h : i.byteIdx < s.bsize
⊢ ¬s.startPos + i = s.stopPos

Tactic:
case a =>
  refine mt (congrArg String.Pos.byteIdx) (Nat.ne_of_lt ?_)
  exact (Nat.add_comm .. ▸ Nat.add_lt_of_lt_sub h :)

Result:
s : Substring
i : String.Pos
h : i.byteIdx < s.bsize
⊢ i.byteIdx < { byteIdx := (s.str.next (s.startPos + i)).byteIdx - s.startPos.byteIdx }.byteIdx
-- Mathlib/MeasureTheory/Decomposition/Exhaustion.lean
@[measurability]
lemma measurableSet_sigmaFiniteSetWRT :
    MeasurableSet (μ.sigmaFiniteSetWRT ν)

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
⊢ MeasurableSet
    (if h : ∃ s, MeasurableSet s ∧ SigmaFinite (μ.restrict s) ∧ ∀ t ⊆ sᶜ, ν t ≠ 0 → μ t = ⊤ then h.choose else ∅)

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ∃ s, MeasurableSet s ∧ SigmaFinite (μ.restrict s) ∧ ∀ t ⊆ sᶜ, ν t ≠ 0 → μ t = ⊤
⊢ MeasurableSet h.choose

case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ¬∃ s, MeasurableSet s ∧ SigmaFinite (μ.restrict s) ∧ ∀ t ⊆ sᶜ, ν t ≠ 0 → μ t = ⊤
⊢ MeasurableSet ∅

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
⊢ MeasurableSet (μ.sigmaFiniteSetWRT ν)

Tactic:
rw [Measure.sigmaFiniteSetWRT]

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
⊢ MeasurableSet
    (if h : ∃ s, MeasurableSet s ∧ SigmaFinite (μ.restrict s) ∧ ∀ t ⊆ sᶜ, ν t ≠ 0 → μ t = ⊤ then h.choose else ∅)

Proof state:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ¬∃ s, MeasurableSet s ∧ SigmaFinite (μ.restrict s) ∧ ∀ t ⊆ sᶜ, ν t ≠ 0 → μ t = ⊤
⊢ MeasurableSet ∅

Tactic:
exact MeasurableSet.empty

Result:
no goals

Proof state:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ∃ s, MeasurableSet s ∧ SigmaFinite (μ.restrict s) ∧ ∀ t ⊆ sᶜ, ν t ≠ 0 → μ t = ⊤
⊢ MeasurableSet h.choose

Tactic:
exact h.choose_spec.1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Bootstrap.lean
theorem append_empty (as : Array α) : as ++ #[] = as

Proof state:
case h
α : Type u_1
as : Array α
⊢ (as ++ #[]).toList = as.toList

Tactic:
simp only [toList_append, toList_empty, List.append_nil]

Result:
no goals

Proof state:
α : Type u_1
as : Array α
⊢ as ++ #[] = as

Tactic:
apply ext'

Result:
case h
α : Type u_1
as : Array α
⊢ (as ++ #[]).toList = as.toList
-- Mathlib/RingTheory/Regular/IsSMulRegular.lean
lemma IsSMulRegular.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul :
    IsSMulRegular M r → (IsSMulRegular (M ⧸ N) r ↔ r • ⊤ ⊓ N ≤ r • N)

Proof state:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
h : Function.Injective ⇑(DistribMulAction.toLinearMap R M r)
⊢ map ((LinearMap.lsmul R M) r) ⊤ ⊓ N ≤ map ((LinearMap.lsmul R M) r) N ↔ r • ⊤ ⊓ N ≤ r • N

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
h : Function.Injective ⇑(DistribMulAction.toLinearMap R M r)
⊢ IsSMulRegular (M ⧸ N) r ↔ r • ⊤ ⊓ N ≤ r • N

Tactic:
rw [isSMulRegular_on_quot_iff_lsmul_comap_le, ← map_le_map_iff_of_injective h,
  ← LinearMap.lsmul_eq_DistribMulAction_toLinearMap,
  map_comap_eq, LinearMap.range_eq_map]

Result:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
h : Function.Injective ⇑(DistribMulAction.toLinearMap R M r)
⊢ map ((LinearMap.lsmul R M) r) ⊤ ⊓ N ≤ map ((LinearMap.lsmul R M) r) N ↔ r • ⊤ ⊓ N ≤ r • N

Proof state:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
⊢ IsSMulRegular M r → (IsSMulRegular (M ⧸ N) r ↔ r • ⊤ ⊓ N ≤ r • N)

Tactic:
intro (h : Function.Injective (DistribMulAction.toLinearMap R M r))

Result:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
h : Function.Injective ⇑(DistribMulAction.toLinearMap R M r)
⊢ IsSMulRegular (M ⧸ N) r ↔ r • ⊤ ⊓ N ≤ r • N
-- Mathlib/Algebra/Homology/HomologicalBicomplex.lean
lemma shape_f (K : HomologicalComplex₂ C c₁ c₂) (i₁ i₁' : I₁) (h : ¬ c₁.Rel i₁ i₁') (i₂ : I₂) :
    (K.d i₁ i₁').f i₂ = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
i₁ i₁' : I₁
h : ¬c₁.Rel i₁ i₁'
i₂ : I₂
⊢ (K.d i₁ i₁').f i₂ = 0

Tactic:
rw [K.shape _ _ h, zero_f]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean
theorem of_s_of_int (a : ℤ) : (of (a : K)).s = Stream'.Seq.nil :=
  haveI h : ∀ n, (of (a : K)).s.get? n = none

Proof state:
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
a : ℤ
⊢ (of ↑a).s.get? 0 = none

Tactic:
rw [of_s_head_aux, stream_succ_of_int, Option.bind]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
a : ℤ
⊢ ∀ (n : ℕ), (of ↑a).s.get? n = none

Tactic:
intro n

Result:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
a : ℤ
n : ℕ
⊢ (of ↑a).s.get? n = none

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
a : ℤ
n : ℕ
⊢ (of ↑a).s.get? n = none

Tactic:
induction n with
| zero => rw [of_s_head_aux, stream_succ_of_int, Option.bind]
| succ n ih => exact (of (a : K)).s.prop ih

Result:
no goals

Proof state:
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
a : ℤ
n : ℕ
ih : (of ↑a).s.get? n = none
⊢ (of ↑a).s.get? (n + 1) = none

Tactic:
exact (of (a : K)).s.prop ih

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem comap_iInf {ι β} (f : α → β) (m : ι → OuterMeasure β) :
    comap f (⨅ i, m i) = ⨅ i, comap f (m i)

Proof state:
α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
m : ι → OuterMeasure β
s : Set α
hs : s.Nonempty
t : ℕ → Set β
ht : s ⊆ ⋃ i, f ⁻¹' t i
k : ℕ
⊢ ⨅ i, (m i) (f '' (f ⁻¹' t k)) ≤ ⨅ i, (m i) (t k)

Tactic:
exact iInf_mono fun i => (m i).mono (image_preimage_subset _ _)

Result:
no goals

Proof state:
α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
m : ι → OuterMeasure β
⊢ (comap f) (⨅ i, m i) = ⨅ i, (comap f) (m i)

Tactic:
refine ext_nonempty fun s hs => ?_

Result:
α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
m : ι → OuterMeasure β
s : Set α
hs : s.Nonempty
⊢ ((comap f) (⨅ i, m i)) s = (⨅ i, (comap f) (m i)) s

Proof state:
α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
m : ι → OuterMeasure β
s : Set α
hs : s.Nonempty
⊢ (⨅ i, (comap f) (m i)) s ≤ ((comap f) (⨅ i, m i)) s

Tactic:
simp only [comap_apply, iInf_apply' _ hs, iInf_apply' _ (hs.image _), le_iInf_iff,
  Set.image_subset_iff, preimage_iUnion]

Result:
α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
m : ι → OuterMeasure β
s : Set α
hs : s.Nonempty
⊢ ∀ (i : ℕ → Set β),
    s ⊆ ⋃ i_1, f ⁻¹' i i_1 →
      ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i, (m i) (f '' t n) ≤ ∑' (n : ℕ), ⨅ i_2, (m i_2) (i n)

Proof state:
α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
m : ι → OuterMeasure β
s : Set α
hs : s.Nonempty
⊢ ((comap f) (⨅ i, m i)) s = (⨅ i, (comap f) (m i)) s

Tactic:
refine ((comap_mono f).map_iInf_le s).antisymm ?_

Result:
α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
m : ι → OuterMeasure β
s : Set α
hs : s.Nonempty
⊢ (⨅ i, (comap f) (m i)) s ≤ ((comap f) (⨅ i, m i)) s

Proof state:
α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
m : ι → OuterMeasure β
s : Set α
hs : s.Nonempty
⊢ ∀ (i : ℕ → Set β),
    s ⊆ ⋃ i_1, f ⁻¹' i i_1 →
      ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i, (m i) (f '' t n) ≤ ∑' (n : ℕ), ⨅ i_2, (m i_2) (i n)

Tactic:
refine fun t ht => iInf_le_of_le _ (iInf_le_of_le ht <| ENNReal.tsum_le_tsum fun k => ?_)

Result:
α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
m : ι → OuterMeasure β
s : Set α
hs : s.Nonempty
t : ℕ → Set β
ht : s ⊆ ⋃ i, f ⁻¹' t i
k : ℕ
⊢ ⨅ i, (m i) (f '' (f ⁻¹' t k)) ≤ ⨅ i, (m i) (t k)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem getElem_mapIdx (f : Nat → α → β) (a : Vector α n) (i : Nat) (h : i < n) :
    (a.mapIdx f)[i] = f i (a[i]'(by simp_all))

Proof state:
α : Type u_1
β : Type u_2
n : Nat
f : Nat → α → β
a : Vector α n
i : Nat
h : i < n
⊢ (mapIdx f a)[i] = f i a[i]

Tactic:
rcases a with ⟨a, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : Nat → α → β
i : Nat
a : Array α
h : i < a.size
⊢ (mapIdx f { toArray := a, size_toArray := ⋯ })[i] = f i { toArray := a, size_toArray := ⋯ }[i]

Proof state:
α : Type ?u.4191
β : Type ?u.4213
n : Nat
f : Nat → α → β
a : Vector α n
i : Nat
h : i < n
⊢ i < n

Tactic:
simp_all

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
f : Nat → α → β
i : Nat
a : Array α
h : i < a.size
⊢ (mapIdx f { toArray := a, size_toArray := ⋯ })[i] = f i { toArray := a, size_toArray := ⋯ }[i]

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem isUnit_det {A : Type*} [CommRing A] [Module A M] (f : M →ₗ[A] M) (hf : IsUnit f) :
    IsUnit (LinearMap.det f)

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
A : Type u_7
inst✝¹ : CommRing A
inst✝ : Module A M
f : M →ₗ[A] M
hf : IsUnit f
⊢ IsUnit (LinearMap.det f)

Tactic:
obtain ⟨g, hg⟩ : ∃ g, f.comp g = 1 := hf.exists_right_inv

Result:
case intro
M : Type u_2
inst✝² : AddCommGroup M
A : Type u_7
inst✝¹ : CommRing A
inst✝ : Module A M
f : M →ₗ[A] M
hf : IsUnit f
g : M →ₗ[A] M
hg : f ∘ₗ g = 1
⊢ IsUnit (LinearMap.det f)

Proof state:
case intro
M : Type u_2
inst✝² : AddCommGroup M
A : Type u_7
inst✝¹ : CommRing A
inst✝ : Module A M
f : M →ₗ[A] M
hf : IsUnit f
g : M →ₗ[A] M
hg : f ∘ₗ g = 1
⊢ IsUnit (LinearMap.det f)

Tactic:
have : LinearMap.det f * LinearMap.det g = 1 := by
  simp only [← LinearMap.det_comp, hg, MonoidHom.map_one]

Result:
case intro
M : Type u_2
inst✝² : AddCommGroup M
A : Type u_7
inst✝¹ : CommRing A
inst✝ : Module A M
f : M →ₗ[A] M
hf : IsUnit f
g : M →ₗ[A] M
hg : f ∘ₗ g = 1
this : LinearMap.det f * LinearMap.det g = 1
⊢ IsUnit (LinearMap.det f)

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
A : Type u_7
inst✝¹ : CommRing A
inst✝ : Module A M
f : M →ₗ[A] M
hf : IsUnit f
g : M →ₗ[A] M
hg : f ∘ₗ g = 1
⊢ LinearMap.det f * LinearMap.det g = 1

Tactic:
simp only [← LinearMap.det_comp, hg, MonoidHom.map_one]

Result:
no goals

Proof state:
case intro
M : Type u_2
inst✝² : AddCommGroup M
A : Type u_7
inst✝¹ : CommRing A
inst✝ : Module A M
f : M →ₗ[A] M
hf : IsUnit f
g : M →ₗ[A] M
hg : f ∘ₗ g = 1
this : LinearMap.det f * LinearMap.det g = 1
⊢ IsUnit (LinearMap.det f)

Tactic:
exact isUnit_of_mul_eq_one _ _ this

Result:
no goals