harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Sites/Continuous.lean
lemma isContinuous_of_preservesOneHypercovers
    [PreservesOneHypercovers.{w} F J K] [GrothendieckTopology.IsGeneratedByOneHypercovers.{w} J] :
    IsContinuous.{t} F J K where
  op_comp_isSheaf_of_types

Proof state:
case mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : F.PreservesOneHypercovers J K
inst✝ : J.IsGeneratedByOneHypercovers
P : Dᵒᵖ ⥤ Type t
hP : Presheaf.IsSheaf K P
⊢ Presheaf.IsSheaf J (F.op ⋙ { val := P, cond := hP }.val)

Tactic:
exact F.op_comp_isSheaf_of_preservesOneHypercovers J K P hP

Result:
no goals

Proof state:
case mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : F.PreservesOneHypercovers J K
inst✝ : J.IsGeneratedByOneHypercovers
P : Dᵒᵖ ⥤ Type t
hP : Presheaf.IsSheaf K P
⊢ Presieve.IsSheaf J (F.op ⋙ { val := P, cond := hP }.val)

Tactic:
rw [← isSheaf_iff_isSheaf_of_type]

Result:
case mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : F.PreservesOneHypercovers J K
inst✝ : J.IsGeneratedByOneHypercovers
P : Dᵒᵖ ⥤ Type t
hP : Presheaf.IsSheaf K P
⊢ Presheaf.IsSheaf J (F.op ⋙ { val := P, cond := hP }.val)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : F.PreservesOneHypercovers J K
inst✝ : J.IsGeneratedByOneHypercovers
⊢ ∀ (G : Sheaf K (Type t)), Presieve.IsSheaf J (F.op ⋙ G.val)

Tactic:
rintro ⟨P, hP⟩

Result:
case mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : F.PreservesOneHypercovers J K
inst✝ : J.IsGeneratedByOneHypercovers
P : Dᵒᵖ ⥤ Type t
hP : Presheaf.IsSheaf K P
⊢ Presieve.IsSheaf J (F.op ⋙ { val := P, cond := hP }.val)
-- Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean
lemma logTaylor_zero : logTaylor 0 = fun _ ↦ 0

Proof state:
case h
x✝ : ℂ
⊢ logTaylor 0 x✝ = 0

Tactic:
simp only [logTaylor, Finset.range_zero, ← Nat.not_even_iff_odd, Int.cast_pow, Int.cast_neg,
  Int.cast_one, Finset.sum_empty]

Result:
no goals

Proof state:
⊢ logTaylor 0 = fun x => 0

Tactic:
funext

Result:
case h
x✝ : ℂ
⊢ logTaylor 0 x✝ = 0
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem sup_eq_top_iff_isCoprime {R : Type*} [CommSemiring R] (x y : R) :
    span ({x} : Set R) ⊔ span {y} = ⊤ ↔ IsCoprime x y

Proof state:
R : Type u_2
inst✝ : CommSemiring R
x y : R
⊢ span {x} ⊔ span {y} = ⊤ ↔ IsCoprime x y

Tactic:
rw [eq_top_iff_one, Submodule.mem_sup]

Result:
R : Type u_2
inst✝ : CommSemiring R
x y : R
⊢ (∃ y_1 ∈ span {x}, ∃ z ∈ span {y}, y_1 + z = 1) ↔ IsCoprime x y

Proof state:
case mpr
R : Type u_2
inst✝ : CommSemiring R
x y : R
⊢ IsCoprime x y → ∃ y_1 ∈ span {x}, ∃ z ∈ span {y}, y_1 + z = 1

Tactic:
exact fun ⟨u, v, h1⟩ =>
  ⟨_, mem_span_singleton'.mpr ⟨_, rfl⟩, _, mem_span_singleton'.mpr ⟨_, rfl⟩, h1⟩

Result:
no goals

Proof state:
case mp
R : Type u_2
inst✝ : CommSemiring R
x y : R
⊢ (∃ y_1 ∈ span {x}, ∃ z ∈ span {y}, y_1 + z = 1) → IsCoprime x y

Tactic:
rintro ⟨u, hu, v, hv, h1⟩

Result:
case mp.intro.intro.intro.intro
R : Type u_2
inst✝ : CommSemiring R
x y u : R
hu : u ∈ span {x}
v : R
hv : v ∈ span {y}
h1 : u + v = 1
⊢ IsCoprime x y

Proof state:
case mp.intro.intro.intro.intro
R : Type u_2
inst✝ : CommSemiring R
x y u : R
hu : u ∈ span {x}
v : R
hv : v ∈ span {y}
h1 : u + v = 1
⊢ IsCoprime x y

Tactic:
rw [mem_span_singleton'] at hu hv

Result:
case mp.intro.intro.intro.intro
R : Type u_2
inst✝ : CommSemiring R
x y u : R
hu : ∃ a, a * x = u
v : R
hv : ∃ a, a * y = v
h1 : u + v = 1
⊢ IsCoprime x y

Proof state:
R : Type u_2
inst✝ : CommSemiring R
x y : R
⊢ (∃ y_1 ∈ span {x}, ∃ z ∈ span {y}, y_1 + z = 1) ↔ IsCoprime x y

Tactic:
constructor

Result:
case mp
R : Type u_2
inst✝ : CommSemiring R
x y : R
⊢ (∃ y_1 ∈ span {x}, ∃ z ∈ span {y}, y_1 + z = 1) → IsCoprime x y

case mpr
R : Type u_2
inst✝ : CommSemiring R
x y : R
⊢ IsCoprime x y → ∃ y_1 ∈ span {x}, ∃ z ∈ span {y}, y_1 + z = 1

Proof state:
case mp.intro.intro.intro.intro
R : Type u_2
inst✝ : CommSemiring R
x y u : R
hu : ∃ a, a * x = u
v : R
hv : ∃ a, a * y = v
h1 : u + v = 1
⊢ IsCoprime x y

Tactic:
rw [← hu.choose_spec, ← hv.choose_spec] at h1

Result:
case mp.intro.intro.intro.intro
R : Type u_2
inst✝ : CommSemiring R
x y u : R
hu : ∃ a, a * x = u
v : R
hv : ∃ a, a * y = v
h1 : hu.choose * x + hv.choose * y = 1
⊢ IsCoprime x y

Proof state:
case mp.intro.intro.intro.intro
R : Type u_2
inst✝ : CommSemiring R
x y u : R
hu : ∃ a, a * x = u
v : R
hv : ∃ a, a * y = v
h1 : hu.choose * x + hv.choose * y = 1
⊢ IsCoprime x y

Tactic:
exact ⟨_, _, h1⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get_insertMany_list_of_mem [LawfulBEq α] (h : m.1.WF)
    {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l)
    {h'} :
    (m.insertMany l).1.get k' h' = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
h' : (m.insertMany l).val.contains k' = true
⊢ (m.insertMany l).val.get k' h' = cast ⋯ v

Tactic:
simp_to_model [insertMany] using List.getValueCast_insertList_of_mem

Result:
no goals

Proof state:
case e_a
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
h' : (m.insertMany l).val.contains k' = true
⊢ k = k'

Tactic:
apply LawfulBEq.eq_of_beq k_beq

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
h' : (m.insertMany l).val.contains k' = true
⊢ β k = β k'

Tactic:
congr

Result:
case e_a
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
h' : (m.insertMany l).val.contains k' = true
⊢ k = k'
-- Mathlib/Topology/Constructible.lean
lemma IsRetrocompact.finsetInf {ι : Type*} {s : Finset ι} {t : ι → Set X}
    (ht : ∀ i ∈ s, IsRetrocompact (t i)) : IsRetrocompact (s.inf t)

Proof state:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsRetrocompact (t i)) → IsRetrocompact (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)
⊢ i ∈ Finset.cons i s ih

Tactic:
simp

Result:
no goals

Proof state:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
ι : Type u_4
s : Finset ι
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
⊢ IsRetrocompact (s.inf t)

Tactic:
induction s using Finset.cons_induction with
| empty => simp
| cons i s ih hi =>
  rw [Finset.inf_cons]
  exact (ht _ <| by simp).inter <| hi <| Finset.forall_of_forall_cons ht

Result:
no goals

Proof state:
case cons
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsRetrocompact (t i)) → IsRetrocompact (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)
⊢ IsRetrocompact (t i ⊓ s.inf t)

Tactic:
exact (ht _ <| by simp).inter <| hi <| Finset.forall_of_forall_cons ht

Result:
no goals

Proof state:
case empty
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
ι : Type u_4
t : ι → Set X
ht : ∀ i ∈ ∅, IsRetrocompact (t i)
⊢ IsRetrocompact (∅.inf t)

Tactic:
simp

Result:
no goals

Proof state:
case cons
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsRetrocompact (t i)) → IsRetrocompact (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)
⊢ IsRetrocompact ((Finset.cons i s ih).inf t)

Tactic:
rw [Finset.inf_cons]

Result:
case cons
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsRetrocompact (t i)) → IsRetrocompact (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)
⊢ IsRetrocompact (t i ⊓ s.inf t)
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem mul_smul' {A : Type*} [Semiring A] [Algebra R A] (x : T) (p₁ p₂ : LocalizedModule S A) :
    p₁ * x • p₂ = x • (p₁ * p₂)

Proof state:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
⊢ mk a₁ a₂ * x • mk s₁ s₂ = x • (mk a₁ a₂ * mk s₁ s₂)

Tactic:
rw [smul_def, mk_mul_mk, mk_mul_mk, smul_def, mul_left_comm, mul_smul_comm]

Result:
no goals

Proof state:
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : T
p₁ p₂ : LocalizedModule S A
⊢ p₁ * x • p₂ = x • (p₁ * p₂)

Tactic:
induction p₁, p₂ using induction_on₂ with | _ a₁ s₁ a₂ s₂ => _

Result:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
⊢ mk a₁ a₂ * x • mk s₁ s₂ = x • (mk a₁ a₂ * mk s₁ s₂)
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem eval_multiset_prod_X_sub_C_derivative [DecidableEq R]
    {S : Multiset R} {r : R} (hr : r ∈ S) :
    eval r (derivative (Multiset.map (fun a => X - C a) S).prod) =
      (Multiset.map (fun a => r - a) (S.erase r)).prod

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : DecidableEq R
S : Multiset R
r : R
hr : r ∈ S
this :
  ↑(evalRingHom r) (Multiset.map (fun a => X - C a) (S.erase r)).prod =
    (Multiset.map (⇑↑(evalRingHom r)) (Multiset.map (fun a => X - C a) (S.erase r))).prod
⊢ eval r (derivative (Multiset.map (fun a => X - C a) (r ::ₘ S.erase r)).prod) =
    (Multiset.map (fun a => r - a) (S.erase r)).prod

Tactic:
simpa using this

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : DecidableEq R
S : Multiset R
r : R
hr : r ∈ S
⊢ eval r (derivative (Multiset.map (fun a => X - C a) S).prod) = (Multiset.map (fun a => r - a) (S.erase r)).prod

Tactic:
nth_rw 1 [← Multiset.cons_erase hr]

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : DecidableEq R
S : Multiset R
r : R
hr : r ∈ S
⊢ eval r (derivative (Multiset.map (fun a => X - C a) (r ::ₘ S.erase r)).prod) =
    (Multiset.map (fun a => r - a) (S.erase r)).prod

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : DecidableEq R
S : Multiset R
r : R
hr : r ∈ S
⊢ eval r (derivative (Multiset.map (fun a => X - C a) (r ::ₘ S.erase r)).prod) =
    (Multiset.map (fun a => r - a) (S.erase r)).prod

Tactic:
have := (evalRingHom r).map_multiset_prod (Multiset.map (fun a => X - C a) (S.erase r))

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : DecidableEq R
S : Multiset R
r : R
hr : r ∈ S
this :
  ↑(evalRingHom r) (Multiset.map (fun a => X - C a) (S.erase r)).prod =
    (Multiset.map (⇑↑(evalRingHom r)) (Multiset.map (fun a => X - C a) (S.erase r))).prod
⊢ eval r (derivative (Multiset.map (fun a => X - C a) (r ::ₘ S.erase r)).prod) =
    (Multiset.map (fun a => r - a) (S.erase r)).prod
-- Mathlib/CategoryTheory/EpiMono.lean
theorem isIso_of_mono_of_isSplitEpi {X Y : C} (f : X ⟶ Y) [Mono f] [IsSplitEpi f] : IsIso f :=
  ⟨⟨section_ f, ⟨by simp [← cancel_mono f], by simp⟩⟩⟩

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : IsSplitEpi f
⊢ section_ f ≫ f = 𝟙 Y

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : IsSplitEpi f
⊢ f ≫ section_ f = 𝟙 X

Tactic:
simp [← cancel_mono f]

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem _root_.Pairwise.exists_mem_filter_basis_of_disjoint {I} [Finite I] {l : I → Filter α}
    {ι : I → Sort*} {p : ∀ i, ι i → Prop} {s : ∀ i, ι i → Set α} (hd : Pairwise (Disjoint on l))
    (h : ∀ i, (l i).HasBasis (p i) (s i)) :
    ∃ ind : ∀ i, ι i, (∀ i, p i (ind i)) ∧ Pairwise (Disjoint on fun i => s i (ind i))

Proof state:
α : Type u_1
I : Type u_7
inst✝ : Finite I
l : I → Filter α
ι : I → Sort u_6
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
hd : Pairwise (Disjoint on l)
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
⊢ ∃ ind, (∀ (i : I), p i (ind i)) ∧ Pairwise (Disjoint on fun i => s i (ind i))

Tactic:
rcases hd.exists_mem_filter_of_disjoint with ⟨t, htl, hd⟩

Result:
case intro.intro
α : Type u_1
I : Type u_7
inst✝ : Finite I
l : I → Filter α
ι : I → Sort u_6
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
hd✝ : Pairwise (Disjoint on l)
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
t : I → Set α
htl : ∀ (i : I), t i ∈ l i
hd : Pairwise (Disjoint on t)
⊢ ∃ ind, (∀ (i : I), p i (ind i)) ∧ Pairwise (Disjoint on fun i => s i (ind i))

Proof state:
case intro.intro
α : Type u_1
I : Type u_7
inst✝ : Finite I
l : I → Filter α
ι : I → Sort u_6
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
hd✝ : Pairwise (Disjoint on l)
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
t : I → Set α
htl : ∀ (i : I), t i ∈ l i
hd : Pairwise (Disjoint on t)
ind : (i : I) → ι i
hp : ∀ (i : I), p i (ind i)
ht : ∀ (i : I), s i (ind i) ⊆ t i
⊢ ∃ ind, (∀ (i : I), p i (ind i)) ∧ Pairwise (Disjoint on fun i => s i (ind i))

Tactic:
exact ⟨ind, hp, hd.mono fun i j hij => hij.mono (ht _) (ht _)⟩

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
I : Type u_7
inst✝ : Finite I
l : I → Filter α
ι : I → Sort u_6
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
hd✝ : Pairwise (Disjoint on l)
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
t : I → Set α
htl : ∀ (i : I), t i ∈ l i
hd : Pairwise (Disjoint on t)
⊢ ∃ ind, (∀ (i : I), p i (ind i)) ∧ Pairwise (Disjoint on fun i => s i (ind i))

Tactic:
choose ind hp ht using fun i => (h i).mem_iff.1 (htl i)

Result:
case intro.intro
α : Type u_1
I : Type u_7
inst✝ : Finite I
l : I → Filter α
ι : I → Sort u_6
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
hd✝ : Pairwise (Disjoint on l)
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
t : I → Set α
htl : ∀ (i : I), t i ∈ l i
hd : Pairwise (Disjoint on t)
ind : (i : I) → ι i
hp : ∀ (i : I), p i (ind i)
ht : ∀ (i : I), s i (ind i) ⊆ t i
⊢ ∃ ind, (∀ (i : I), p i (ind i)) ∧ Pairwise (Disjoint on fun i => s i (ind i))
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem ofBool_congr (b : Bool) (e' : BitVec 1) (h : e' = BitVec.ofBool b) : e'.getLsbD 0 = b

Proof state:
b : Bool
e' : BitVec 1
h : e' = BitVec.ofBool b
⊢ e'.getLsbD 0 = b

Tactic:
cases b <;> simp [h]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem card_eq_nrRealPlaces_add_nrComplexPlaces :
    Fintype.card (InfinitePlace K) = nrRealPlaces K + nrComplexPlaces K

Proof state:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
⊢ card (InfinitePlace K) = nrRealPlaces K + nrComplexPlaces K

Tactic:
convert Fintype.card_subtype_or_disjoint (IsReal (K := K)) (IsComplex (K := K))
  (disjoint_isReal_isComplex K) using 1

Result:
case h.e'_2
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
⊢ card (InfinitePlace K) = card { x // x.IsReal ∨ x.IsComplex }

Proof state:
case h.e'_2
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
⊢ card (InfinitePlace K) = card { x // x.IsReal ∨ x.IsComplex }

Tactic:
exact (Fintype.card_of_subtype _ (fun w ↦ ⟨fun _ ↦ isReal_or_isComplex w, fun _ ↦ by simp⟩)).symm

Result:
no goals

Proof state:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
x✝ : w.IsReal ∨ w.IsComplex
⊢ w ∈ Finset.univ

Tactic:
simp

Result:
no goals

Proof state:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
⊢ card (InfinitePlace K) = nrRealPlaces K + nrComplexPlaces K

Tactic:
classical
convert Fintype.card_subtype_or_disjoint (IsReal (K := K)) (IsComplex (K := K))
  (disjoint_isReal_isComplex K) using 1
exact (Fintype.card_of_subtype _ (fun w ↦ ⟨fun _ ↦ isReal_or_isComplex w, fun _ ↦ by simp⟩)).symm

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Sort.lean
theorem monotone_proj (f : Fin n → α) : Monotone (graph.proj : graph f → α)

Proof state:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Monotone graph.proj

Tactic:
rintro ⟨⟨x, i⟩, hx⟩ ⟨⟨y, j⟩, hy⟩ (_ | h)

Result:
case mk.mk.mk.mk.left
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
x : α
i : Fin n
hx : (x, i) ∈ graph f
y : α
j : Fin n
hy : (y, j) ∈ graph f
h✝ : x < y
⊢ graph.proj ⟨(x, i), hx⟩ ≤ graph.proj ⟨(y, j), hy⟩

case mk.mk.mk.mk.right
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
x : α
i : Fin n
hx : (x, i) ∈ graph f
j : Fin n
hy : (x, j) ∈ graph f
h✝ : i ≤ j
⊢ graph.proj ⟨(x, i), hx⟩ ≤ graph.proj ⟨(x, j), hy⟩

Proof state:
case mk.mk.mk.mk.left
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
x : α
i : Fin n
hx : (x, i) ∈ graph f
y : α
j : Fin n
hy : (y, j) ∈ graph f
h✝ : x < y
⊢ graph.proj ⟨(x, i), hx⟩ ≤ graph.proj ⟨(y, j), hy⟩

Tactic:
exact le_of_lt ‹_›

Result:
no goals

Proof state:
case mk.mk.mk.mk.right
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
x : α
i : Fin n
hx : (x, i) ∈ graph f
j : Fin n
hy : (x, j) ∈ graph f
h✝ : i ≤ j
⊢ graph.proj ⟨(x, i), hx⟩ ≤ graph.proj ⟨(x, j), hy⟩

Tactic:
simp [graph.proj]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean
theorem incMatrix_apply_eq_zero_iff : G.incMatrix R a e = 0 ↔ e ∉ G.incidenceSet a

Proof state:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a : α
e : Sym2 α
inst✝ : Nontrivial R
⊢ incMatrix R G a e = 0 ↔ e ∉ G.incidenceSet a

Tactic:
simp only [incMatrix_apply, Set.indicator_apply_eq_zero, Pi.one_apply, one_ne_zero]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
@[simp]
lemma φ_two : W.φ 2 = C X * W.ψ₂ ^ 2 - C W.Ψ₃

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 2 - 1 = 1

Tactic:
rfl

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.φ 2 = C X * W.ψ₂ ^ 2 - C W.Ψ₃

Tactic:
rw [φ, ψ_two, two_add_one_eq_three, ψ_three, show (2 - 1 : ℤ) = 1 by rfl, ψ_one, mul_one]

Result:
no goals
-- Mathlib/Order/CompleteBooleanAlgebra.lean
lemma sSup_inf_eq : sSup s ⊓ b = ⨆ a ∈ s, a ⊓ b

Proof state:
α : Type u
minAx : MinimalAxioms α
s : Set α
b : α
⊢ sSup s ⊓ b = ⨆ a ∈ s, a ⊓ b

Tactic:
simpa only [inf_comm] using @inf_sSup_eq α _ s b

Result:
no goals
-- Mathlib/NumberTheory/FLT/Basic.lean
lemma fermatLastTheoremFor_zero : FermatLastTheoremFor 0 :=
  fun _ _ _ _ _ _ ↦ by norm_num

Proof state:
x✝⁵ x✝⁴ x✝³ : ℕ
x✝² : x✝⁵ ≠ 0
x✝¹ : x✝⁴ ≠ 0
x✝ : x✝³ ≠ 0
⊢ x✝⁵ ^ 0 + x✝⁴ ^ 0 ≠ x✝³ ^ 0

Tactic:
norm_num

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addU_smul {P Q : Fin 3 → F} (hPz : P z ≠ 0) (hQz : Q z ≠ 0) {u v : F} (hu : u ≠ 0)
    (hv : v ≠ 0) : addU (u • P) (v • Q) = (u * v) ^ 2 * addU P Q

Proof state:
F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
u v : F
hu : u ≠ 0
hv : v ≠ 0
⊢ (u * P y * (v * Q z) - v * Q y * (u * P z)) ^ 3 * (P z * Q z) =
    (u * v) ^ 2 * (P y * Q z - Q y * P z) ^ 3 * (u * P z * (v * Q z))

Tactic:
ring1

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
u v : F
hu : u ≠ 0
hv : v ≠ 0
⊢ addU (u • P) (v • Q) = (u * v) ^ 2 * addU P Q

Tactic:
field_simp [addU, smul_fin3_ext]

Result:
F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
u v : F
hu : u ≠ 0
hv : v ≠ 0
⊢ (u * P y * (v * Q z) - v * Q y * (u * P z)) ^ 3 * (P z * Q z) =
    (u * v) ^ 2 * (P y * Q z - Q y * P z) ^ 3 * (u * P z * (v * Q z))
-- Mathlib/Order/KrullDimension.lean
lemma height_le_iff {a : α} {n : ℕ∞} :
    height a ≤ n ↔ ∀ ⦃p : LTSeries α⦄, p.last ≤ a → p.length ≤ n

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ height a ≤ n ↔ ∀ ⦃p : LTSeries α⦄, RelSeries.last p ≤ a → ↑p.length ≤ n

Tactic:
rw [height, iSup₂_le_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
theorem add_neg {X Y : C} (a b : X ⟶ Y) : a + -b = a - b

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ a + -b = a - b

Tactic:
rw [add_def, neg_neg]

Result:
no goals
-- Mathlib/GroupTheory/Submonoid/Center.lean
theorem MulOpposite.op_mem_center_iff [Mul M] {x : M} :
    op x ∈ Set.center Mᵐᵒᵖ ↔ x ∈ Set.center M

Proof state:
M : Type u_2
inst✝ : Mul M
x : M
⊢ op x ∈ Set.center Mᵐᵒᵖ ↔ x ∈ Set.center M

Tactic:
simp_rw [Set.mem_center_iff, isMulCentral_iff, MulOpposite.forall, ← op_mul, op_inj]

Result:
M : Type u_2
inst✝ : Mul M
x : M
⊢ ((∀ (a : M), a * x = x * a) ∧
      (∀ (a a_1 : M), a_1 * a * x = a_1 * (a * x)) ∧
        (∀ (a a_1 : M), a_1 * (x * a) = a_1 * x * a) ∧ ∀ (a a_1 : M), x * (a_1 * a) = x * a_1 * a) ↔
    (∀ (a : M), x * a = a * x) ∧
      (∀ (b c : M), x * (b * c) = x * b * c) ∧
        (∀ (a c : M), a * x * c = a * (x * c)) ∧ ∀ (a b : M), a * b * x = a * (b * x)

Proof state:
M : Type u_2
inst✝ : Mul M
x : M
⊢ ((∀ (a : M), a * x = x * a) ∧
      (∀ (a a_1 : M), a_1 * a * x = a_1 * (a * x)) ∧
        (∀ (a a_1 : M), a_1 * (x * a) = a_1 * x * a) ∧ ∀ (a a_1 : M), x * (a_1 * a) = x * a_1 * a) ↔
    (∀ (a : M), x * a = a * x) ∧
      (∀ (b c : M), x * (b * c) = x * b * c) ∧
        (∀ (a c : M), a * x * c = a * (x * c)) ∧ ∀ (a b : M), a * b * x = a * (b * x)

Tactic:
aesop

Result:
no goals
-- Mathlib/FieldTheory/Perfect.lean
theorem roots_expand_pow_image_iterateFrobenius_subset [DecidableEq R] :
    (expand R (p ^ n) f).roots.toFinset.image (iterateFrobenius R p n) ⊆ f.roots.toFinset

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : DecidableEq R
⊢ Multiset.map (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots ⊆ p ^ n • f.roots

Tactic:
exact subset_of_le (roots_expand_pow_map_iterateFrobenius_le p n f)

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : DecidableEq R
⊢ Finset.image (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots.toFinset ⊆ f.roots.toFinset

Tactic:
rw [Finset.image_toFinset, ← (roots f).toFinset_nsmul _ (expChar_pow_pos R p n).ne',
  toFinset_subset]

Result:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : DecidableEq R
⊢ Multiset.map (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots ⊆ p ^ n • f.roots