harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem_eq_iff {l : List α} {i : Nat} {h : i < l.length} : l[i] = x ↔ l[i]? = some x

Proof state:
α : Type u_1
x : α
l : List α
i : Nat
h : i < l.length
⊢ l[i] = x ↔ ∃ h, l[i] = x

Tactic:
exact ⟨fun w => ⟨h, w⟩, fun h => h.2⟩

Result:
no goals

Proof state:
α : Type u_1
x : α
l : List α
i : Nat
h : i < l.length
⊢ l[i] = x ↔ l[i]? = some x

Tactic:
simp only [getElem?_eq_some_iff]

Result:
α : Type u_1
x : α
l : List α
i : Nat
h : i < l.length
⊢ l[i] = x ↔ ∃ h, l[i] = x
-- Mathlib/RingTheory/WittVector/Verschiebung.lean
theorem map_verschiebung (f : R →+* S) (x : 𝕎 R) :
    map f (verschiebung x) = verschiebung (map f x)

Proof state:
p : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
⊢ (map f) (verschiebung x) = verschiebung ((map f) x)

Tactic:
ext ⟨-, -⟩

Result:
case h.zero
p : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
⊢ ((map f) (verschiebung x)).coeff 0 = (verschiebung ((map f) x)).coeff 0

case h.succ
p : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
n✝ : ℕ
⊢ ((map f) (verschiebung x)).coeff (n✝ + 1) = (verschiebung ((map f) x)).coeff (n✝ + 1)

Proof state:
case h.succ
p : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
n✝ : ℕ
⊢ ((map f) (verschiebung x)).coeff (n✝ + 1) = (verschiebung ((map f) x)).coeff (n✝ + 1)

Tactic:
rfl

Result:
no goals

Proof state:
case h.zero
p : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
⊢ ((map f) (verschiebung x)).coeff 0 = (verschiebung ((map f) x)).coeff 0

Tactic:
exact f.map_zero

Result:
no goals
-- Mathlib/Combinatorics/Additive/DoublingConst.lean
lemma cast_subConst_mul_card (A B : Finset G') : (δ[A, B] * #A : 𝕜) = #(A - B)

Proof state:
G' : Type u_2
inst✝³ : AddGroup G'
inst✝² : DecidableEq G'
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G'
⊢ δ[A, B] * ↑(#A) = ↑(#(A - B))

Tactic:
exact subConst_mul_card _ _

Result:
no goals

Proof state:
G' : Type u_2
inst✝³ : AddGroup G'
inst✝² : DecidableEq G'
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G'
⊢ ↑δ[A, B] * ↑(#A) = ↑(#(A - B))

Tactic:
norm_cast

Result:
G' : Type u_2
inst✝³ : AddGroup G'
inst✝² : DecidableEq G'
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G'
⊢ δ[A, B] * ↑(#A) = ↑(#(A - B))
-- Mathlib/Order/Filter/AtTopBot/CountablyGenerated.lean
theorem frequently_iff_seq_frequently {ι : Type*} {l : Filter ι} {p : ι → Prop}
    [l.IsCountablyGenerated] :
    (∃ᶠ n in l, p n) ↔ ∃ x : ℕ → ι, Tendsto x atTop l ∧ ∃ᶠ n : ℕ in atTop, p (x n)

Proof state:
ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
⊢ (∃ x, Tendsto x atTop l ∧ ¬∀ᶠ (n : ℕ) in atTop, ¬p (x n)) ↔
    ∃ x, Tendsto x atTop l ∧ ¬∀ᶠ (x_1 : ℕ) in atTop, ¬p (x x_1)

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
⊢ (¬∀ (x : ℕ → ι), Tendsto x atTop l → ∀ᶠ (n : ℕ) in atTop, ¬p (x n)) ↔
    ∃ x, Tendsto x atTop l ∧ ¬∀ᶠ (x_1 : ℕ) in atTop, ¬p (x x_1)

Tactic:
push_neg

Result:
ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
⊢ (∃ x, Tendsto x atTop l ∧ ¬∀ᶠ (n : ℕ) in atTop, ¬p (x n)) ↔
    ∃ x, Tendsto x atTop l ∧ ¬∀ᶠ (x_1 : ℕ) in atTop, ¬p (x x_1)

Proof state:
ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
⊢ (∃ᶠ (n : ι) in l, p n) ↔ ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)

Tactic:
simp only [Filter.Frequently, eventually_iff_seq_eventually (l := l)]

Result:
ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
⊢ (¬∀ (x : ℕ → ι), Tendsto x atTop l → ∀ᶠ (n : ℕ) in atTop, ¬p (x n)) ↔
    ∃ x, Tendsto x atTop l ∧ ¬∀ᶠ (x_1 : ℕ) in atTop, ¬p (x x_1)
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
theorem zeta_sub_one_prime_of_ne_two [IsCyclotomicExtension {p ^ (k + 1)} ℚ K]
    (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) (hodd : p ≠ 2) :
    Prime (hζ.toInteger - 1)

Proof state:
case refine_1
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K := numberField {p ^ (k + 1)} ℚ K
h : hζ.toInteger - 1 = 0
⊢ ζ ^ 1 = 1

Tactic:
rw [sub_eq_zero] at h

Result:
case refine_1
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K := numberField {p ^ (k + 1)} ℚ K
h : hζ.toInteger = 1
⊢ ζ ^ 1 = 1
-- Mathlib/Algebra/Divisibility/Units.lean
theorem IsRelPrime.mul_left (H1 : IsRelPrime x z) (H2 : IsRelPrime y z) : IsRelPrime (x * y) z :=
  fun _ h hz ↦ by
    obtain ⟨a, b, ha, hb, rfl⟩ := exists_dvd_and_dvd_of_dvd_mul h
    exact (H1 ha <| (dvd_mul_right a b).trans hz).mul (H2 hb <| (dvd_mul_left b a).trans hz)

Proof state:
α : Type u_1
inst✝¹ : CommMonoid α
x y z : α
inst✝ : DecompositionMonoid α
H1 : IsRelPrime x z
H2 : IsRelPrime y z
x✝ : α
h : x✝ ∣ x * y
hz : x✝ ∣ z
⊢ IsUnit x✝

Tactic:
obtain ⟨a, b, ha, hb, rfl⟩ := exists_dvd_and_dvd_of_dvd_mul h

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommMonoid α
x y z : α
inst✝ : DecompositionMonoid α
H1 : IsRelPrime x z
H2 : IsRelPrime y z
a b : α
ha : a ∣ x
hb : b ∣ y
h : a * b ∣ x * y
hz : a * b ∣ z
⊢ IsUnit (a * b)

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommMonoid α
x y z : α
inst✝ : DecompositionMonoid α
H1 : IsRelPrime x z
H2 : IsRelPrime y z
a b : α
ha : a ∣ x
hb : b ∣ y
h : a * b ∣ x * y
hz : a * b ∣ z
⊢ IsUnit (a * b)

Tactic:
exact (H1 ha <| (dvd_mul_right a b).trans hz).mul (H2 hb <| (dvd_mul_left b a).trans hz)

Result:
no goals
-- Mathlib/CategoryTheory/Subpresheaf/OfSection.lean
lemma ofSection_eq_range {X : Cᵒᵖ} (x : F.obj X) :
    ofSection x = range (yonedaEquiv.symm x)

Proof state:
case obj.h.h.mp.intro
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
f : X ⟶ U
⊢ ∃ y, (yonedaEquiv.symm x).app U y = F.map f x

Tactic:
exact ⟨f.unop, rfl⟩

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : Cᵒᵖ
x : F.obj X
⊢ ofSection x = range (yonedaEquiv.symm x)

Tactic:
ext U y

Result:
case obj.h.h
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ y ∈ (ofSection x).obj U ↔ y ∈ (range (yonedaEquiv.symm x)).obj U

Proof state:
case obj.h.h
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ y ∈ (ofSection x).obj U ↔ y ∈ (range (yonedaEquiv.symm x)).obj U

Tactic:
simp only [ofSection_obj, Set.mem_setOf_eq, Opposite.op_unop, range_obj, yoneda_obj_obj,
  Set.mem_range]

Result:
case obj.h.h
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ (∃ f, F.map f x = y) ↔ ∃ y_1, (yonedaEquiv.symm x).app U y_1 = y

Proof state:
case obj.h.h.mpr.intro
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
f : Opposite.unop U ⟶ Opposite.unop X
⊢ ∃ f_1, F.map f_1 x = (yonedaEquiv.symm x).app U f

Tactic:
exact ⟨f.op, rfl⟩

Result:
no goals

Proof state:
case obj.h.h.mpr
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ (∃ y_1, (yonedaEquiv.symm x).app U y_1 = y) → ∃ f, F.map f x = y

Tactic:
rintro ⟨f, rfl⟩

Result:
case obj.h.h.mpr.intro
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
f : Opposite.unop U ⟶ Opposite.unop X
⊢ ∃ f_1, F.map f_1 x = (yonedaEquiv.symm x).app U f

Proof state:
case obj.h.h
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ (∃ f, F.map f x = y) ↔ ∃ y_1, (yonedaEquiv.symm x).app U y_1 = y

Tactic:
constructor

Result:
case obj.h.h.mp
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ (∃ f, F.map f x = y) → ∃ y_1, (yonedaEquiv.symm x).app U y_1 = y

case obj.h.h.mpr
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ (∃ y_1, (yonedaEquiv.symm x).app U y_1 = y) → ∃ f, F.map f x = y

Proof state:
case obj.h.h.mp
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ (∃ f, F.map f x = y) → ∃ y_1, (yonedaEquiv.symm x).app U y_1 = y

Tactic:
rintro ⟨f, rfl⟩

Result:
case obj.h.h.mp.intro
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
f : X ⟶ U
⊢ ∃ y, (yonedaEquiv.symm x).app U y = F.map f x
-- Mathlib/Algebra/Divisibility/Units.lean
theorem dvd (hu : IsUnit u) : u ∣ a

Proof state:
case intro
α : Type u_1
inst✝ : Monoid α
a : α
u : αˣ
⊢ ↑u ∣ a

Tactic:
apply Units.coe_dvd

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Monoid α
a u : α
hu : IsUnit u
⊢ u ∣ a

Tactic:
rcases hu with ⟨u, rfl⟩

Result:
case intro
α : Type u_1
inst✝ : Monoid α
a : α
u : αˣ
⊢ ↑u ∣ a
-- Mathlib/Order/GaloisConnection/Basic.lean
theorem l_sInf_u_image [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u)
    (s : Set β) : l (sInf (u '' s)) = sInf s

Proof state:
α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
s : Set β
⊢ l (sInf (u '' s)) = sInf s

Tactic:
rw [sInf_image, gi.l_biInf_u, sInf_eq_iInf]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem image_iInter {f : α → β} (hf : Bijective f) (s : ι → Set α) :
    (f '' ⋂ i, s i) = ⋂ i, f '' s i

Proof state:
case inl
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
hf : Bijective f
s : ι → Set α
h✝ : IsEmpty ι
⊢ f '' ⋂ i, s i = ⋂ i, f '' s i

Tactic:
simp_rw [iInter_of_empty, image_univ_of_surjective hf.surjective]

Result:
no goals

Proof state:
case inr
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
hf : Bijective f
s : ι → Set α
h✝ : Nonempty ι
⊢ f '' ⋂ i, s i = ⋂ i, f '' s i

Tactic:
exact hf.injective.injOn.image_iInter_eq

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
hf : Bijective f
s : ι → Set α
⊢ f '' ⋂ i, s i = ⋂ i, f '' s i

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
hf : Bijective f
s : ι → Set α
h✝ : IsEmpty ι
⊢ f '' ⋂ i, s i = ⋂ i, f '' s i

case inr
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
hf : Bijective f
s : ι → Set α
h✝ : Nonempty ι
⊢ f '' ⋂ i, s i = ⋂ i, f '' s i
-- Mathlib/Algebra/Divisibility/Units.lean
theorem isRelPrime_mul_unit_left_right : IsRelPrime y (x * z) ↔ IsRelPrime y z

Proof state:
α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime y (x * z) ↔ IsRelPrime y z

Tactic:
rw [isRelPrime_comm, isRelPrime_mul_unit_left_left hu, isRelPrime_comm]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/HashMap/WF.lean
theorem WF.out [BEq α] [Hashable α] {m : Imp α β} (h : m.WF) :
    m.size = m.buckets.size ∧ m.buckets.WF

Proof state:
case empty'
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
n✝ : Nat
h : 0 < n✝
⊢ (Imp.empty' n✝ h).size = (Imp.empty' n✝ h).buckets.size ∧ (Imp.empty' n✝ h).buckets.WF

Tactic:
exact ⟨(Buckets.mk_size h).symm, .mk' h⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
h : m.WF
⊢ m.size = m.buckets.size ∧ m.buckets.WF

Tactic:
induction h with
| mk h₁ h₂ => exact ⟨h₁, h₂⟩
| @empty' _ h => exact ⟨(Buckets.mk_size h).symm, .mk' h⟩
| insert _ ih => exact ⟨insert_size ih.1, insert_WF ih.2⟩
| erase _ ih => exact ⟨erase_size ih.1, erase_WF ih.2⟩
| modify _ ih => exact ⟨modify_size ih.1, modify_WF ih.2⟩

Result:
no goals

Proof state:
case insert
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m m✝ : Imp α β
a✝¹ : α
b✝ : β
a✝ : m✝.WF
ih : m✝.size = m✝.buckets.size ∧ m✝.buckets.WF
⊢ (m✝.insert a✝¹ b✝).size = (m✝.insert a✝¹ b✝).buckets.size ∧ (m✝.insert a✝¹ b✝).buckets.WF

Tactic:
exact ⟨insert_size ih.1, insert_WF ih.2⟩

Result:
no goals

Proof state:
case erase
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m m✝ : Imp α β
a✝¹ : α
a✝ : m✝.WF
ih : m✝.size = m✝.buckets.size ∧ m✝.buckets.WF
⊢ (m✝.erase a✝¹).size = (m✝.erase a✝¹).buckets.size ∧ (m✝.erase a✝¹).buckets.WF

Tactic:
exact ⟨erase_size ih.1, erase_WF ih.2⟩

Result:
no goals

Proof state:
case modify
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m m✝ : Imp α β
a✝¹ : α
f✝ : α → β → β
a✝ : m✝.WF
ih : m✝.size = m✝.buckets.size ∧ m✝.buckets.WF
⊢ (m✝.modify a✝¹ f✝).size = (m✝.modify a✝¹ f✝).buckets.size ∧ (m✝.modify a✝¹ f✝).buckets.WF

Tactic:
exact ⟨modify_size ih.1, modify_WF ih.2⟩

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m m✝ : Imp α β
h₁ : m✝.size = m✝.buckets.size
h₂ : m✝.buckets.WF
⊢ m✝.size = m✝.buckets.size ∧ m✝.buckets.WF

Tactic:
exact ⟨h₁, h₂⟩

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Unique.lean
theorem leftAdjointUniq_refl {F : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) :
    (leftAdjointUniq adj1 adj1).hom = 𝟙 _

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
⊢ (adj1.leftAdjointUniq adj1).hom = 𝟙 F

Tactic:
simp [leftAdjointUniq]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_const_sub_Iic : (fun x => a - x) '' Iic b = Ici (a - b)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
⊢ (fun x => a - x) '' Iic b = Ici (a - b)

Tactic:
have := image_comp (fun x => a + x) fun x => -x

Result:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Iic b = Ici (a - b)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Iic b = Ici (a - b)

Tactic:
simp [sub_eq_add_neg, this, add_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Iic b = Ici (a - b)

Tactic:
dsimp [Function.comp_def] at this

Result:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Iic b = Ici (a - b)
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
@[simp]
lemma map_isoClosure (P : MorphismProperty C) (F : C ⥤ D) :
    P.isoClosure.map F = P.map F

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty C
F : C ⥤ D
⊢ P.isoClosure.map F = P.map F

Tactic:
apply le_antisymm

Result:
case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty C
F : C ⥤ D
⊢ P.isoClosure.map F ≤ P.map F

case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty C
F : C ⥤ D
⊢ P.map F ≤ P.isoClosure.map F

Proof state:
case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty C
F : C ⥤ D
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e : Arrow.mk f' ≅ Arrow.mk f
⊢ (P.map F).inverseImage F f

Tactic:
exact ⟨_, _, f', hf', ⟨F.mapArrow.mapIso e⟩⟩

Result:
no goals

Proof state:
case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty C
F : C ⥤ D
⊢ P.isoClosure ≤ (P.map F).inverseImage F

Tactic:
intro X Y f ⟨X', Y', f', hf', ⟨e⟩⟩

Result:
case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty C
F : C ⥤ D
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e : Arrow.mk f' ≅ Arrow.mk f
⊢ (P.map F).inverseImage F f

Proof state:
case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty C
F : C ⥤ D
⊢ P.isoClosure.map F ≤ P.map F

Tactic:
rw [map_le_iff]

Result:
case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty C
F : C ⥤ D
⊢ P.isoClosure ≤ (P.map F).inverseImage F

Proof state:
case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty C
F : C ⥤ D
⊢ P.map F ≤ P.isoClosure.map F

Tactic:
exact monotone_map _ (le_isoClosure P)

Result:
no goals
-- Mathlib/Data/Fintype/EquivFin.lean
theorem Finite.of_injective {α β : Sort*} [Finite β] (f : α → β) (H : Injective f) : Finite α

Proof state:
case intro.intro
α : Sort u_4
β : Sort u_5
inst✝ : Finite β
f : α → β
H : Injective f
n : ℕ
e : β ≃ Fin n
⊢ Finite α

Tactic:
classical exact .of_equiv (Set.range (e ∘ f)) (Equiv.ofInjective _ (e.injective.comp H)).symm

Result:
no goals

Proof state:
case intro.intro
α : Sort u_4
β : Sort u_5
inst✝ : Finite β
f : α → β
H : Injective f
n : ℕ
e : β ≃ Fin n
⊢ Finite α

Tactic:
exact .of_equiv (Set.range (e ∘ f)) (Equiv.ofInjective _ (e.injective.comp H)).symm

Result:
no goals

Proof state:
α : Sort u_4
β : Sort u_5
inst✝ : Finite β
f : α → β
H : Injective f
⊢ Finite α

Tactic:
rcases Finite.exists_equiv_fin β with ⟨n, ⟨e⟩⟩

Result:
case intro.intro
α : Sort u_4
β : Sort u_5
inst✝ : Finite β
f : α → β
H : Injective f
n : ℕ
e : β ≃ Fin n
⊢ Finite α
-- Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean
theorem of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none :
    (of v).TerminatedAt n ↔ IntFractPair.stream v (n + 1) = none

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ (of v).TerminatedAt n ↔ IntFractPair.stream v (n + 1) = none

Tactic:
rw [of_terminatedAt_iff_intFractPair_seq1_terminatedAt, Stream'.Seq.TerminatedAt,
  IntFractPair.get?_seq1_eq_succ_get?_stream]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem j_of_isShortNF_of_char_three [CharP F 3] : W.j = 0

Proof state:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsShortNF
inst✝ : CharP F 3
⊢ W.j = 0

Tactic:
rw [j, c₄_of_isShortNF_of_char_three]

Result:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsShortNF
inst✝ : CharP F 3
⊢ ↑W.Δ'⁻¹ * 0 ^ 3 = 0

Proof state:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsShortNF
inst✝ : CharP F 3
⊢ ↑W.Δ'⁻¹ * 0 ^ 3 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Ideal/Nonunits.lean
theorem exists_max_ideal_of_mem_nonunits [CommSemiring α] (h : a ∈ nonunits α) :
    ∃ I : Ideal α, I.IsMaximal ∧ a ∈ I

Proof state:
α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
⊢ Ideal.span {a} ≠ ⊤

Tactic:
intro H

Result:
α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
H : Ideal.span {a} = ⊤
⊢ False

Proof state:
case intro.intro
α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
I : Ideal α
Imax : I.IsMaximal
H : Ideal.span {a} ≤ I
⊢ ∃ I, I.IsMaximal ∧ a ∈ I

Tactic:
use I, Imax

Result:
case right
α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
I : Ideal α
Imax : I.IsMaximal
H : Ideal.span {a} ≤ I
⊢ a ∈ I

Proof state:
case right
α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
I : Ideal α
Imax : I.IsMaximal
H : Ideal.span {a} ≤ I
⊢ a ∈ I

Tactic:
apply H

Result:
case right.a
α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
I : Ideal α
Imax : I.IsMaximal
H : Ideal.span {a} ≤ I
⊢ a ∈ Ideal.span {a}

Proof state:
α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
H : Ideal.span {a} = ⊤
⊢ False

Tactic:
rw [Ideal.span_singleton_eq_top] at H

Result:
α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
H : IsUnit a
⊢ False

Proof state:
α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
⊢ ∃ I, I.IsMaximal ∧ a ∈ I

Tactic:
rcases Ideal.exists_le_maximal _ this with ⟨I, Imax, H⟩

Result:
case intro.intro
α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
I : Ideal α
Imax : I.IsMaximal
H : Ideal.span {a} ≤ I
⊢ ∃ I, I.IsMaximal ∧ a ∈ I

Proof state:
α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
⊢ ∃ I, I.IsMaximal ∧ a ∈ I

Tactic:
have : Ideal.span ({a} : Set α) ≠ ⊤ := by
  intro H
  rw [Ideal.span_singleton_eq_top] at H
  contradiction

Result:
α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
⊢ ∃ I, I.IsMaximal ∧ a ∈ I

Proof state:
α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
H : IsUnit a
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
case right.a.a
α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
I : Ideal α
Imax : I.IsMaximal
H : Ideal.span {a} ≤ I
⊢ a ∈ {a}

Tactic:
exact Set.mem_singleton a

Result:
no goals

Proof state:
case right.a
α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
I : Ideal α
Imax : I.IsMaximal
H : Ideal.span {a} ≤ I
⊢ a ∈ Ideal.span {a}

Tactic:
apply Ideal.subset_span

Result:
case right.a.a
α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
I : Ideal α
Imax : I.IsMaximal
H : Ideal.span {a} ≤ I
⊢ a ∈ {a}
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_eq_get? [LawfulBEq α] (h : m.WF) {a : α} : get? m a = m.get? a

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝ : LawfulBEq α
h : m.WF
a : α
⊢ get? m a = m.get? a

Tactic:
simp_to_raw using Raw₀.Const.get?_eq_get?

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem lt_floor_add_one (a : α) : a < ⌊a⌋₊ + 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
⊢ a < ↑⌊a⌋₊ + 1

Tactic:
simpa using lt_succ_floor a

Result:
no goals
-- Mathlib/Tactic/NormNum/LegendreSymbol.lean
theorem jacobiSymNat.one_left (b : ℕ) : jacobiSymNat 1 b = 1

Proof state:
b : ℕ
⊢ jacobiSymNat 1 b = 1

Tactic:
rw [jacobiSymNat, Nat.cast_one, jacobiSym.one_left]

Result:
no goals
-- Mathlib/FieldTheory/Laurent.lean
theorem laurentAux_div :
    laurentAux r (algebraMap _ _ p / algebraMap _ _ q) =
      algebraMap _ _ (taylor r p) / algebraMap _ _ (taylor r q) :=
  -- Porting note: added `by exact taylor_mem_nonZeroDivisors r`
  map_apply_div _ (by exact taylor_mem_nonZeroDivisors r) _ _

Proof state:
R : Type u
inst✝¹ : CommRing R
r : R
p q : R[X]
inst✝ : IsDomain R
⊢ R[X]⁰ ≤ Submonoid.comap { toFun := ⇑(taylor r), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } R[X]⁰

Tactic:
exact taylor_mem_nonZeroDivisors r

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/Projections.lean
theorem P_add_Q (q : ℕ) : P q + Q q = 𝟙 K[X]

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ P q + (𝟙 K[X] - P q) = 𝟙 K[X]

Tactic:
abel

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ P q + Q q = 𝟙 K[X]

Tactic:
rw [Q]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ P q + (𝟙 K[X] - P q) = 𝟙 K[X]