harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem exists_mem_eq_sup' (f : ι → α) : ∃ i, i ∈ s ∧ s.sup' H f = f i

Proof state:
case cons.intro.intro.inr
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s✝ : Finset ι
H : s✝.Nonempty
f : ι → α
c : ι
s : Finset ι
hcs : c ∉ s
hs : s.Nonempty
b : ι
hb : b ∈ s
h' : s.sup' hs f = f b
h : f c ≤ f b
⊢ ∃ i ∈ cons c s hcs, f c ⊔ f b = f i

Tactic:
exact ⟨b, mem_cons.2 (Or.inr hb), sup_eq_right.2 h⟩

Result:
no goals

Proof state:
case cons
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s✝ : Finset ι
H : s✝.Nonempty
f : ι → α
c : ι
s : Finset ι
hcs : c ∉ s
hs : s.Nonempty
ih : ∃ i ∈ s, s.sup' hs f = f i
⊢ ∃ i ∈ cons c s hcs, (cons c s hcs).sup' ⋯ f = f i

Tactic:
rcases ih with ⟨b, hb, h'⟩

Result:
case cons.intro.intro
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s✝ : Finset ι
H : s✝.Nonempty
f : ι → α
c : ι
s : Finset ι
hcs : c ∉ s
hs : s.Nonempty
b : ι
hb : b ∈ s
h' : s.sup' hs f = f b
⊢ ∃ i ∈ cons c s hcs, (cons c s hcs).sup' ⋯ f = f i

Proof state:
case singleton
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
c : ι
⊢ ∃ i ∈ {c}, {c}.sup' ⋯ f = f i

Tactic:
exact ⟨c, mem_singleton_self c, rfl⟩

Result:
no goals

Proof state:
case cons.intro.intro.inl
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s✝ : Finset ι
H : s✝.Nonempty
f : ι → α
c : ι
s : Finset ι
hcs : c ∉ s
hs : s.Nonempty
b : ι
hb : b ∈ s
h' : s.sup' hs f = f b
h : f b ≤ f c
⊢ ∃ i ∈ cons c s hcs, f c ⊔ f b = f i

Tactic:
exact ⟨c, mem_cons.2 (Or.inl rfl), sup_eq_left.2 h⟩

Result:
no goals

Proof state:
case cons.intro.intro
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s✝ : Finset ι
H : s✝.Nonempty
f : ι → α
c : ι
s : Finset ι
hcs : c ∉ s
hs : s.Nonempty
b : ι
hb : b ∈ s
h' : s.sup' hs f = f b
⊢ ∃ i ∈ cons c s hcs, f c ⊔ f b = f i

Tactic:
cases le_total (f b) (f c) with
| inl h => exact ⟨c, mem_cons.2 (Or.inl rfl), sup_eq_left.2 h⟩
| inr h => exact ⟨b, mem_cons.2 (Or.inr hb), sup_eq_right.2 h⟩

Result:
no goals

Proof state:
case cons.intro.intro
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s✝ : Finset ι
H : s✝.Nonempty
f : ι → α
c : ι
s : Finset ι
hcs : c ∉ s
hs : s.Nonempty
b : ι
hb : b ∈ s
h' : s.sup' hs f = f b
⊢ ∃ i ∈ cons c s hcs, (cons c s hcs).sup' ⋯ f = f i

Tactic:
rw [sup'_cons hs, h']

Result:
case cons.intro.intro
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s✝ : Finset ι
H : s✝.Nonempty
f : ι → α
c : ι
s : Finset ι
hcs : c ∉ s
hs : s.Nonempty
b : ι
hb : b ∈ s
h' : s.sup' hs f = f b
⊢ ∃ i ∈ cons c s hcs, f c ⊔ f b = f i

Proof state:
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
⊢ ∃ i ∈ s, s.sup' H f = f i

Tactic:
induction H using Finset.Nonempty.cons_induction with
| singleton c =>  exact ⟨c, mem_singleton_self c, rfl⟩
| cons c s hcs hs ih =>
  rcases ih with ⟨b, hb, h'⟩
  rw [sup'_cons hs, h']
  cases le_total (f b) (f c) with
  | inl h => exact ⟨c, mem_cons.2 (Or.inl rfl), sup_eq_left.2 h⟩
  | inr h => exact ⟨b, mem_cons.2 (Or.inr hb), sup_eq_right.2 h⟩

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_cos_add_sin_mul_I_sub (θ : ℝ) :
    arg (cos θ + sin θ * I) - θ = 2 * π * ⌊(π - θ) / (2 * π)⌋

Proof state:
θ : ℝ
⊢ (cos ↑θ + sin ↑θ * I).arg - θ = 2 * π * ↑⌊(π - θ) / (2 * π)⌋

Tactic:
rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I_sub zero_lt_one]

Result:
no goals
-- Mathlib/Algebra/Lie/TensorProduct.lean
theorem lie_tmul_right (x : L) (m : M) (n : N) : ⁅x, m ⊗ₜ[R] n⁆ = ⁅x, m⁆ ⊗ₜ n + m ⊗ₜ ⁅x, n⁆ :=
  show hasBracketAux x (m ⊗ₜ[R] n) = _ by
    simp only [hasBracketAux, LinearMap.rTensor_tmul, toEnd_apply_apply,
      LinearMap.add_apply, LinearMap.lTensor_tmul]

Proof state:
R : Type u
inst✝¹⁰ : CommRing R
L : Type v
M : Type w
N : Type w₁
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
x : L
m : M
n : N
⊢ (hasBracketAux x) (m ⊗ₜ[R] n) = ⁅x, m⁆ ⊗ₜ[R] n + m ⊗ₜ[R] ⁅x, n⁆

Tactic:
simp only [hasBracketAux, LinearMap.rTensor_tmul, toEnd_apply_apply,
  LinearMap.add_apply, LinearMap.lTensor_tmul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem umod_one {x : BitVec w} : x % (1#w) = 0#w

Proof state:
w : Nat
x : BitVec w
⊢ x % 1#w = 0#w

Tactic:
simp only [toNat_eq, toNat_umod, toNat_ofNat, Nat.zero_mod]

Result:
w : Nat
x : BitVec w
⊢ x.toNat % (1 % 2 ^ w) = 0

Proof state:
case zero
x : BitVec 0
⊢ x.toNat % (1 % 2 ^ 0) = 0

Tactic:
simp [eq_nil x]

Result:
no goals

Proof state:
case succ
n✝ : Nat
x : BitVec (n✝ + 1)
⊢ x.toNat % (1 % 2 ^ (n✝ + 1)) = 0

Tactic:
simp [Nat.mod_one]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ x.toNat % (1 % 2 ^ w) = 0

Tactic:
cases w

Result:
case zero
x : BitVec 0
⊢ x.toNat % (1 % 2 ^ 0) = 0

case succ
n✝ : Nat
x : BitVec (n✝ + 1)
⊢ x.toNat % (1 % 2 ^ (n✝ + 1)) = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem tail_replicate (n : Nat) (a : α) : (replicate n a).tail = replicate (n - 1) a

Proof state:
α : Type u_1
n : Nat
a : α
⊢ (replicate n a).tail = replicate (n - 1) a

Tactic:
cases n <;> simp [replicate_succ]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma IsPerfectMatching.induce_connectedComponent_isMatching (h : M.IsPerfectMatching)
    (c : ConnectedComponent G) : (M.induce c.supp).IsMatching

Proof state:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsPerfectMatching
c : G.ConnectedComponent
⊢ (M.induce c.supp).IsMatching

Tactic:
simpa [h.2.verts_eq_univ] using h.1.induce_connectedComponent c

Result:
no goals
-- Mathlib/Analysis/Analytic/Composition.lean
theorem compChangeOfVariables_length (m M N : ℕ) {i : Σ n, Fin n → ℕ}
    (hi : i ∈ compPartialSumSource m M N) :
    Composition.length (compChangeOfVariables m M N i hi).2 = i.1

Proof state:
case mk
m M N k : ℕ
blocks_fun : Fin k → ℕ
hi : ⟨k, blocks_fun⟩ ∈ compPartialSumSource m M N
⊢ (compChangeOfVariables m M N ⟨k, blocks_fun⟩ hi).snd.length = ⟨k, blocks_fun⟩.fst

Tactic:
dsimp [compChangeOfVariables]

Result:
case mk
m M N k : ℕ
blocks_fun : Fin k → ℕ
hi : ⟨k, blocks_fun⟩ ∈ compPartialSumSource m M N
⊢ { blocks := ofFn fun a => blocks_fun a, blocks_pos := ⋯, blocks_sum := ⋯ }.length = k

Proof state:
case mk
m M N k : ℕ
blocks_fun : Fin k → ℕ
hi : ⟨k, blocks_fun⟩ ∈ compPartialSumSource m M N
⊢ { blocks := ofFn fun a => blocks_fun a, blocks_pos := ⋯, blocks_sum := ⋯ }.length = k

Tactic:
simp only [Composition.length, map_ofFn, length_ofFn]

Result:
no goals

Proof state:
m M N : ℕ
i : (n : ℕ) × (Fin n → ℕ)
hi : i ∈ compPartialSumSource m M N
⊢ (compChangeOfVariables m M N i hi).snd.length = i.fst

Tactic:
rcases i with ⟨k, blocks_fun⟩

Result:
case mk
m M N k : ℕ
blocks_fun : Fin k → ℕ
hi : ⟨k, blocks_fun⟩ ∈ compPartialSumSource m M N
⊢ (compChangeOfVariables m M N ⟨k, blocks_fun⟩ hi).snd.length = ⟨k, blocks_fun⟩.fst
-- Mathlib/RingTheory/Coprime/Basic.lean
lemma abs_right_iff (x y : R) : IsCoprime x |y| ↔ IsCoprime x y

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : AddLeftMono R
x y : R
⊢ IsCoprime x |y| ↔ IsCoprime x y

Tactic:
rw [isCoprime_comm, IsCoprime.abs_left_iff, isCoprime_comm]

Result:
no goals
-- Mathlib/RingTheory/Adjoin/Field.lean
theorem minpoly_neg_splits [Algebra K L] {x : L} (g : (minpoly K x).Splits (algebraMap K L)) :
    (minpoly K (-x)).Splits (algebraMap K L)

Proof state:
K : Type u_2
L : Type u_3
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
g : Splits (algebraMap K L) (minpoly K x)
⊢ Splits (algebraMap K L) ((-1) ^ (minpoly K x).natDegree)

Tactic:
simpa only [map_pow, map_neg, map_one] using
  splits_C (algebraMap K L) ((-1) ^ (minpoly K x).natDegree)

Result:
no goals

Proof state:
K : Type u_2
L : Type u_3
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
g : Splits (algebraMap K L) (minpoly K x)
⊢ Splits (algebraMap K L) ((-1) ^ (minpoly K x).natDegree * (minpoly K x).comp (-X))

Tactic:
apply splits_mul _ _ g.comp_neg_X

Result:
K : Type u_2
L : Type u_3
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
g : Splits (algebraMap K L) (minpoly K x)
⊢ Splits (algebraMap K L) ((-1) ^ (minpoly K x).natDegree)

Proof state:
K : Type u_2
L : Type u_3
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
g : Splits (algebraMap K L) (minpoly K x)
⊢ Splits (algebraMap K L) (minpoly K (-x))

Tactic:
rw [minpoly.neg]

Result:
K : Type u_2
L : Type u_3
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
g : Splits (algebraMap K L) (minpoly K x)
⊢ Splits (algebraMap K L) ((-1) ^ (minpoly K x).natDegree * (minpoly K x).comp (-X))
-- Mathlib/Data/Finsupp/Basic.lean
theorem eq_zero_of_comapDomain_eq_zero [AddCommMonoid M] (f : α → β) (l : β →₀ M)
    (hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support) : comapDomain f l hf.injOn = 0 → l = 0

Proof state:
case intro
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
h : ∀ (a : α), f a ∉ l.support
a : β
ha : a ∈ l.support
b : α
hb : b ∈ f ⁻¹' ↑l.support ∧ f b = a
⊢ False

Tactic:
exact h b (hb.2.symm ▸ ha)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
⊢ (∀ (a : α), f a ∉ l.support) → ∀ (a : β), a ∉ l.support

Tactic:
intro h a ha

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
h : ∀ (a : α), f a ∉ l.support
a : β
ha : a ∈ l.support
⊢ False

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
⊢ comapDomain f l ⋯ = 0 → l = 0

Tactic:
rw [← support_eq_empty, ← support_eq_empty, comapDomain]

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
⊢ { support := l.support.preimage f ⋯, toFun := fun a => l (f a), mem_support_toFun := ⋯ }.support = ∅ → l.support = ∅

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
h : ∀ (a : α), f a ∉ l.support
a : β
ha : a ∈ l.support
⊢ False

Tactic:
obtain ⟨b, hb⟩ := hf.2.2 ha

Result:
case intro
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
h : ∀ (a : α), f a ∉ l.support
a : β
ha : a ∈ l.support
b : α
hb : b ∈ f ⁻¹' ↑l.support ∧ f b = a
⊢ False

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
⊢ { support := l.support.preimage f ⋯, toFun := fun a => l (f a), mem_support_toFun := ⋯ }.support = ∅ → l.support = ∅

Tactic:
simp only [Finset.ext_iff, Finset.not_mem_empty, iff_false, mem_preimage]

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
⊢ (∀ (a : α), f a ∉ l.support) → ∀ (a : β), a ∉ l.support
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_ofBool (b : Bool) (i : Nat) : (ofBool b).getLsbD i = ((i = 0) && b)

Proof state:
case true
i : Nat
⊢ (ofBool true).getLsbD i = (decide (i = 0) && true)

Tactic:
simp only [ofBool, ofNat_eq_ofNat, cond_true, getLsbD_ofNat, Bool.and_true]

Result:
case true
i : Nat
⊢ (decide (i < 1) && Nat.testBit 1 i) = decide (i = 0)

Proof state:
b : Bool
i : Nat
⊢ (ofBool b).getLsbD i = (decide (i = 0) && b)

Tactic:
rcases b with rfl | rfl

Result:
case false
i : Nat
⊢ (ofBool false).getLsbD i = (decide (i = 0) && false)

case true
i : Nat
⊢ (ofBool true).getLsbD i = (decide (i = 0) && true)

Proof state:
case true
i : Nat
⊢ (decide (i < 1) && Nat.testBit 1 i) = decide (i = 0)

Tactic:
by_cases hi : i = 0 <;> simp [hi] <;> omega

Result:
no goals

Proof state:
case false
i : Nat
⊢ (ofBool false).getLsbD i = (decide (i = 0) && false)

Tactic:
simp [ofBool]

Result:
no goals
-- Mathlib/Data/Nat/Cast/Order/Basic.lean
theorem one_le_cast : 1 ≤ (n : α) ↔ 1 ≤ n

Proof state:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ 1 ≤ ↑n ↔ 1 ≤ n

Tactic:
rw [← cast_one, cast_le]

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean
theorem isBasis_basicOpen :
    TopologicalSpace.Opens.IsBasis (Set.range (basicOpen 𝒜))

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ TopologicalSpace.Opens.IsBasis (Set.range (basicOpen 𝒜))

Tactic:
delta TopologicalSpace.Opens.IsBasis

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ TopologicalSpace.IsTopologicalBasis (SetLike.coe '' Set.range (basicOpen 𝒜))

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ TopologicalSpace.IsTopologicalBasis (SetLike.coe '' Set.range (basicOpen 𝒜))

Tactic:
convert ProjectiveSpectrum.isTopologicalBasis_basic_opens 𝒜

Result:
case h.e'_3.h
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
e_1✝ : ↑↑(Proj 𝒜).toPresheafedSpace = ProjectiveSpectrum 𝒜
⊢ SetLike.coe '' Set.range (basicOpen 𝒜) = Set.range fun r => ↑(ProjectiveSpectrum.basicOpen 𝒜 r)

Proof state:
case h.e'_3.h
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
e_1✝ : ↑↑(Proj 𝒜).toPresheafedSpace = ProjectiveSpectrum 𝒜
⊢ SetLike.coe '' Set.range (basicOpen 𝒜) = Set.range fun r => ↑(ProjectiveSpectrum.basicOpen 𝒜 r)

Tactic:
exact (Set.range_comp _ _).symm

Result:
no goals
-- Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean
lemma isIso_lanAdjunction_counit_app_iff (G : D ⥤ H) :
    IsIso ((L.lanAdjunction H).counit.app G) ↔ G.IsLeftKanExtension (𝟙 (L ⋙ G)) :=
  (isLeftKanExtension_iff_isIso _ (L.lanUnit.app (L ⋙ G)) _ (by simp)).symm

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_6, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{u_5, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
G : D ⥤ H
⊢ L.lanUnit.app (L ⋙ G) ≫ whiskerLeft L ((L.lanAdjunction H).counit.app G) = 𝟙 (L ⋙ G)

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/FLT/Three.lean
private lemma isCoprime_Y_Z : IsCoprime S.Y S.Z

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ IsCoprime (FermatLastTheoremForThreeGen.Solution.y S) (FermatLastTheoremForThreeGen.Solution.z S)

Tactic:
exact isCoprime_y_z S

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ 0 < 3

Tactic:
decide

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ IsCoprime (FermatLastTheoremForThreeGen.Solution.Y S) (FermatLastTheoremForThreeGen.Solution.Z S)

Tactic:
rw [← IsCoprime.pow_iff (m := 3) (n := 3) (by decide) (by decide),
  ← isCoprime_mul_unit_right_left S.u₂.isUnit, ← isCoprime_mul_unit_right_right S.u₃.isUnit,
  Y_u₂_spec, Z_u₃_spec]

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ IsCoprime (FermatLastTheoremForThreeGen.Solution.y S) (FermatLastTheoremForThreeGen.Solution.z S)
-- Mathlib/CategoryTheory/Sites/DenseSubsite/Basic.lean
lemma Functor.is_cover_of_isCoverDense (G : C ⥤ D) (K : GrothendieckTopology D)
    [G.IsCoverDense K] (U : D) : Sieve.coverByImage G U ∈ K U

Proof state:
C : Type u_1
inst✝² : Category.{u_4, u_1} C
D : Type u_2
inst✝¹ : Category.{u_5, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝ : G.IsCoverDense K
U : D
⊢ Sieve.coverByImage G U ∈ K U

Tactic:
apply Functor.IsCoverDense.is_cover

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean
theorem isQuadratic_χ₄ : χ₄.IsQuadratic

Proof state:
⊢ χ₄.IsQuadratic

Tactic:
unfold MulChar.IsQuadratic

Result:
⊢ ∀ (a : ZMod 4), χ₄ a = 0 ∨ χ₄ a = 1 ∨ χ₄ a = -1

Proof state:
⊢ ∀ (a : ZMod 4), χ₄ a = 0 ∨ χ₄ a = 1 ∨ χ₄ a = -1

Tactic:
decide

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ENat.lean
@[simp] lemma ofENat_add_aleph0 (m : ℕ∞) : m + ℵ₀ = ℵ₀

Proof state:
m : ℕ∞
⊢ ↑m + ℵ₀ = ℵ₀

Tactic:
rw [add_comm, aleph0_add_ofENat]

Result:
no goals
-- Mathlib/Algebra/Order/Monovary.lean
@[to_additive (attr := simp)] lemma antivary_inv_right : Antivary f g⁻¹ ↔ Monovary f g

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : OrderedCommGroup α
inst✝ : OrderedCommGroup β
f : ι → α
g : ι → β
⊢ Antivary f g⁻¹ ↔ Monovary f g

Tactic:
simpa [Monovary, Antivary] using forall_swap

Result:
no goals
-- Mathlib/Order/DirectedInverseSystem.lean
theorem exists_eq_mk (z : DirectLimit F f) : ∃ i x, z = ⟦⟨i, x⟩⟧

Proof state:
ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
z : DirectLimit F f
⊢ ∃ i x, z = ⟦⟨i, x⟩⟧

Tactic:
rcases z

Result:
case mk
ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
z : DirectLimit F f
a✝ : (i : ι) × F i
⊢ ∃ i x, Quot.mk (⇑(setoid f)) a✝ = ⟦⟨i, x⟩⟧

Proof state:
case mk
ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
z : DirectLimit F f
a✝ : (i : ι) × F i
⊢ ∃ i x, Quot.mk (⇑(setoid f)) a✝ = ⟦⟨i, x⟩⟧

Tactic:
exact ⟨_, _, rfl⟩

Result:
no goals
-- Mathlib/Order/BooleanSubalgebra.lean
@[simp] lemma mem_iInf {f : ι → BooleanSubalgebra α} : a ∈ ⨅ i, f i ↔ ∀ i, a ∈ f i

Proof state:
ι : Sort u_1
α : Type u_2
inst✝ : BooleanAlgebra α
a : α
f : ι → BooleanSubalgebra α
⊢ a ∈ ⨅ i, f i ↔ ∀ (i : ι), a ∈ f i

Tactic:
rw [← SetLike.mem_coe]

Result:
ι : Sort u_1
α : Type u_2
inst✝ : BooleanAlgebra α
a : α
f : ι → BooleanSubalgebra α
⊢ a ∈ ↑(⨅ i, f i) ↔ ∀ (i : ι), a ∈ f i

Proof state:
ι : Sort u_1
α : Type u_2
inst✝ : BooleanAlgebra α
a : α
f : ι → BooleanSubalgebra α
⊢ a ∈ ↑(⨅ i, f i) ↔ ∀ (i : ι), a ∈ f i

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Preimage.lean
theorem preimage_union [DecidableEq α] [DecidableEq β] {f : α → β} {s t : Finset β} (hst) :
    preimage (s ∪ t) f hst =
      (preimage s f fun _ hx₁ _ hx₂ => hst (mem_union_left _ hx₁) (mem_union_left _ hx₂)) ∪
        preimage t f fun _ hx₁ _ hx₂ => hst (mem_union_right _ hx₁) (mem_union_right _ hx₂) :=
  Finset.coe_injective (by simp)

Proof state:
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s t : Finset β
hst : InjOn f (f ⁻¹' ↑(s ∪ t))
⊢ ↑((s ∪ t).preimage f hst) = ↑(s.preimage f ⋯ ∪ t.preimage f ⋯)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Defs.lean
theorem single_pow [AddMonoid G] {a : G} {b : k} : ∀ n : ℕ, single a b ^ n = single (n • a) (b ^ n)
  | 0 => by
    simp only [pow_zero, zero_nsmul]
    rfl
  | n + 1 => by
    rw [pow_succ, pow_succ, single_pow n, single_mul_single, add_nsmul, one_nsmul]

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : AddMonoid G
a : G
b : k
⊢ single a b ^ 0 = single (0 • a) (b ^ 0)

Tactic:
simp only [pow_zero, zero_nsmul]

Result:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : AddMonoid G
a : G
b : k
⊢ 1 = single 0 1

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : AddMonoid G
a : G
b : k
n : ℕ
⊢ single a b ^ (n + 1) = single ((n + 1) • a) (b ^ (n + 1))

Tactic:
rw [pow_succ, pow_succ, single_pow n, single_mul_single, add_nsmul, one_nsmul]

Result:
no goals

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : AddMonoid G
a : G
b : k
⊢ 1 = single 0 1

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem compl_iInf₂ (f : ∀ i, κ i → UpperSet α) :
    (⨅ (i) (j), f i j).compl = ⨅ (i) (j), (f i j).compl

Proof state:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
f : (i : ι) → κ i → UpperSet α
⊢ (⨅ i, ⨅ j, f i j).compl = ⨅ i, ⨅ j, (f i j).compl

Tactic:
simp_rw [UpperSet.compl_iInf]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma measurable_countableFiltration_densityProcess (κ : Kernel α (γ × β)) (ν : Kernel α γ) (n : ℕ)
    (a : α) {s : Set β} (hs : MeasurableSet s) :
    Measurable[countableFiltration γ n] (fun x ↦ densityProcess κ ν n a x s)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
⊢ Measurable fun x => κ.densityProcess ν n a x s

Tactic:
refine @Measurable.ennreal_toReal _ (countableFiltration γ n) _ ?_

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
⊢ Measurable fun x => (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
⊢ Measurable fun x => (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)

Tactic:
exact (measurable_densityProcess_countableFiltration_aux κ ν n hs).comp measurable_prod_mk_left

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem Const.get!_eq_get!ₘ [BEq α] [Hashable α] [Inhabited β] (m : Raw₀ α (fun _ => β)) (a : α) :
    Const.get! m a = Const.get!ₘ m a

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : Inhabited β
m : Raw₀ α fun x => β
a : α
⊢ get! m a = get!ₘ m a

Tactic:
simp [get!, get!ₘ, get?ₘ, List.getValue!_eq_getValue?, bucket]

Result:
no goals
-- Mathlib/FieldTheory/Cardinality.lean
theorem Infinite.nonempty_field {α : Type u} [Infinite α] : Nonempty (Field α)

Proof state:
α : Type u
inst✝ : Infinite α
⊢ #α = #(FractionRing (MvPolynomial α (ULift.{u, 0} ℚ)))

Tactic:
simp

Result:
no goals