harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Module/Submodule/Lattice.lean
theorem subsingleton_iff_eq_bot : Subsingleton p ↔ p = ⊥

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ Subsingleton ↥p ↔ p = ⊥

Tactic:
rw [subsingleton_iff, Submodule.eq_bot_iff]

Result:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ (∀ (x y : ↥p), x = y) ↔ ∀ x ∈ p, x = 0

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : ∀ (x y : ↥p), x = y
x : M
hx : x ∈ p
⊢ x = 0

Tactic:
simpa using h ⟨x, hx⟩ ⟨0, p.zero_mem⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : ∀ x ∈ p, x = 0
x✝¹ x✝ : ↥p
x : M
hx : x ∈ p
y : M
hy : y ∈ p
⊢ ⟨x, hx⟩ = ⟨y, hy⟩

Tactic:
simp [h x hx, h y hy]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ (∀ (x y : ↥p), x = y) ↔ ∀ x ∈ p, x = 0

Tactic:
refine ⟨fun h x hx ↦ by simpa using h ⟨x, hx⟩ ⟨0, p.zero_mem⟩,
  fun h ⟨x, hx⟩ ⟨y, hy⟩ ↦ by simp [h x hx, h y hy]⟩

Result:
no goals
-- Mathlib/Data/Nat/Totient.lean
theorem totient_eq_iff_prime {p : ℕ} (hp : 0 < p) : p.totient = p - 1 ↔ p.Prime

Proof state:
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ 1 < p

Tactic:
apply lt_of_le_of_ne

Result:
case a
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ 1 ≤ p

case a
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ 1 ≠ p

Proof state:
p : ℕ
hp : 0 < p
⊢ φ p = p - 1 ↔ Prime p

Tactic:
refine ⟨fun h => ?_, totient_prime⟩

Result:
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ Prime p

Proof state:
p : ℕ
h : φ p = p - 1
hp : 1 < p
⊢ Prime p

Tactic:
rw [totient_eq_card_coprime, range_eq_Ico, ← Ico_insert_succ_left hp.le, Finset.filter_insert,
  if_neg (not_coprime_of_dvd_of_dvd hp (dvd_refl p) (dvd_zero p)), ← Nat.card_Ico 1 p] at h

Result:
p : ℕ
h : #(filter (fun a => p.Coprime a) (Ico (succ 0) p)) = #(Ico 1 p)
hp : 1 < p
⊢ Prime p

Proof state:
case a
hp : 0 < 1
h : φ 1 = 1 - 1
⊢ False

Tactic:
rw [totient_one, tsub_self] at h

Result:
case a
hp : 0 < 1
h : 1 = 0
⊢ False

Proof state:
case a
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ 1 ≠ p

Tactic:
rintro rfl

Result:
case a
hp : 0 < 1
h : φ 1 = 1 - 1
⊢ False

Proof state:
p : ℕ
h : #(filter (fun a => p.Coprime a) (Ico (succ 0) p)) = #(Ico 1 p)
hp : 1 < p
n : ℕ
hn : n < p
hnz : n ≠ 0
⊢ succ 0 ≤ n

Tactic:
rwa [succ_le_iff, pos_iff_ne_zero]

Result:
no goals

Proof state:
case a
hp : 0 < 1
h : 1 = 0
⊢ False

Tactic:
exact one_ne_zero h

Result:
no goals

Proof state:
case a
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ 1 ≤ p

Tactic:
rwa [succ_le_iff]

Result:
no goals

Proof state:
p : ℕ
h : #(filter (fun a => p.Coprime a) (Ico (succ 0) p)) = #(Ico 1 p)
hp : 1 < p
⊢ Prime p

Tactic:
refine
  p.prime_of_coprime hp fun n hn hnz => Finset.filter_card_eq h n <| Finset.mem_Ico.mpr ⟨?_, hn⟩

Result:
p : ℕ
h : #(filter (fun a => p.Coprime a) (Ico (succ 0) p)) = #(Ico 1 p)
hp : 1 < p
n : ℕ
hn : n < p
hnz : n ≠ 0
⊢ succ 0 ≤ n
-- Mathlib/Algebra/Polynomial/Lifts.lean
theorem monomial_mem_lifts_and_degree_eq {s : S} {n : ℕ} (hl : monomial n s ∈ lifts f) :
    ∃ q : R[X], map f q = monomial n s ∧ q.degree = (monomial n s).degree

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hl : (monomial n) 0 ∈ lifts f
⊢ map f 0 = (monomial n) 0 ∧ degree 0 = ((monomial n) 0).degree

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
n : ℕ
hl : (monomial n) s ∈ lifts f
⊢ ∃ q, map f q = (monomial n) s ∧ q.degree = ((monomial n) s).degree

Tactic:
rcases eq_or_ne s 0 with rfl | h

Result:
case inl
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hl : (monomial n) 0 ∈ lifts f
⊢ ∃ q, map f q = (monomial n) 0 ∧ q.degree = ((monomial n) 0).degree

case inr
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
n : ℕ
hl : (monomial n) s ∈ lifts f
h : s ≠ 0
⊢ ∃ q, map f q = (monomial n) s ∧ q.degree = ((monomial n) s).degree

Proof state:
case inr
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
n : ℕ
hl : (monomial n) s ∈ lifts f
h : s ≠ 0
⊢ ∃ q, map f q = (monomial n) s ∧ q.degree = ((monomial n) s).degree

Tactic:
obtain ⟨a, rfl⟩ := coeff_monomial_same n s ▸ (monomial n s).lifts_iff_coeff_lifts.mp hl n

Result:
case inr.intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
a : R
hl : (monomial n) (f a) ∈ lifts f
h : f a ≠ 0
⊢ ∃ q, map f q = (monomial n) (f a) ∧ q.degree = ((monomial n) (f a)).degree

Proof state:
case inr.intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
a : R
hl : (monomial n) (f a) ∈ lifts f
h : f a ≠ 0
⊢ ((monomial n) a).degree = ((monomial n) (f a)).degree

Tactic:
rw [degree_monomial, degree_monomial n h]

Result:
case inr.intro.ha
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
a : R
hl : (monomial n) (f a) ∈ lifts f
h : f a ≠ 0
⊢ a ≠ 0

Proof state:
case inr.intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
a : R
hl : (monomial n) (f a) ∈ lifts f
h : f a ≠ 0
⊢ ∃ q, map f q = (monomial n) (f a) ∧ q.degree = ((monomial n) (f a)).degree

Tactic:
refine ⟨monomial n a, map_monomial f, ?_⟩

Result:
case inr.intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
a : R
hl : (monomial n) (f a) ∈ lifts f
h : f a ≠ 0
⊢ ((monomial n) a).degree = ((monomial n) (f a)).degree

Proof state:
case inl
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hl : (monomial n) 0 ∈ lifts f
⊢ ∃ q, map f q = (monomial n) 0 ∧ q.degree = ((monomial n) 0).degree

Tactic:
exact ⟨0, by simp⟩

Result:
no goals

Proof state:
case inr.intro.ha
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
a : R
hl : (monomial n) (f a) ∈ lifts f
h : f a ≠ 0
⊢ a ≠ 0

Tactic:
exact mt (fun ha ↦ ha ▸ map_zero f) h

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/Basic.lean
lemma ringCon_injective : Function.Injective (TwoSidedIdeal.ringCon (R := R))

Proof state:
case mk.mk
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
x : RingCon R
⊢ { ringCon := x } = { ringCon := { ringCon := x }.ringCon }

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
⊢ Function.Injective ringCon

Tactic:
rintro ⟨x⟩ ⟨y⟩ rfl

Result:
case mk.mk
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
x : RingCon R
⊢ { ringCon := x } = { ringCon := { ringCon := x }.ringCon }
-- Mathlib/Topology/Perfect.lean
theorem Preperfect.perfect_closure (hC : Preperfect C) : Perfect (closure C)

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure C
h : x ∉ C
this : {x}ᶜ ∩ C = C
⊢ (𝓝 x ⊓ 𝓟 C).NeBot

Tactic:
rw [closure_eq_cluster_pts] at hx

Result:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ {a | ClusterPt a (𝓟 C)}
h : x ∉ C
this : {x}ᶜ ∩ C = C
⊢ (𝓝 x ⊓ 𝓟 C).NeBot

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure C
h : x ∈ C
⊢ AccPt x (𝓟 C)

Tactic:
exact hC _ h

Result:
no goals

Proof state:
case acc
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
hC : Preperfect C
⊢ Preperfect (closure C)

Tactic:
intro x hx

Result:
case acc
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure C
⊢ AccPt x (𝓟 (closure C))

Proof state:
case closed
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
hC : Preperfect C
⊢ IsClosed (closure C)

Tactic:
exact isClosed_closure

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
hC : Preperfect C
⊢ Perfect (closure C)

Tactic:
constructor

Result:
case closed
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
hC : Preperfect C
⊢ IsClosed (closure C)

case acc
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
hC : Preperfect C
⊢ Preperfect (closure C)

Proof state:
case acc
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure C
⊢ AccPt x (𝓟 (closure C))

Tactic:
by_cases h : x ∈ C <;> apply AccPt.mono _ (principal_mono.mpr subset_closure)

Result:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure C
h : x ∈ C
⊢ AccPt x (𝓟 C)

α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure C
h : x ∉ C
⊢ AccPt x (𝓟 C)

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure C
h : x ∉ C
this : {x}ᶜ ∩ C = C
⊢ AccPt x (𝓟 C)

Tactic:
rw [AccPt, nhdsWithin, inf_assoc, inf_principal, this]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure C
h : x ∉ C
this : {x}ᶜ ∩ C = C
⊢ (𝓝 x ⊓ 𝓟 C).NeBot

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ {a | ClusterPt a (𝓟 C)}
h : x ∉ C
this : {x}ᶜ ∩ C = C
⊢ (𝓝 x ⊓ 𝓟 C).NeBot

Tactic:
exact hx

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure C
h : x ∉ C
⊢ {x}ᶜ ∩ C = C

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure C
h : x ∉ C
⊢ AccPt x (𝓟 C)

Tactic:
have : {x}ᶜ ∩ C = C := by simp [h]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure C
h : x ∉ C
this : {x}ᶜ ∩ C = C
⊢ AccPt x (𝓟 C)
-- Mathlib/NumberTheory/FLT/Four.lean
theorem fermatLastTheoremFour : FermatLastTheoremFor 4

Proof state:
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
a✝ : c ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 4
⊢ a ^ 4 + b ^ 4 = (c ^ 2) ^ 2

Tactic:
rw [heq]

Result:
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
a✝ : c ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 4
⊢ c ^ 4 = (c ^ 2) ^ 2

Proof state:
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
a✝ : c ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 4
⊢ c ^ 4 = (c ^ 2) ^ 2

Tactic:
ring

Result:
no goals

Proof state:
⊢ FermatLastTheoremFor 4

Tactic:
rw [fermatLastTheoremFor_iff_int]

Result:
⊢ FermatLastTheoremWith ℤ 4

Proof state:
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
a✝ : c ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 4
⊢ False

Tactic:
apply @not_fermat_42 _ _ (c ^ 2) ha hb

Result:
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
a✝ : c ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 4
⊢ a ^ 4 + b ^ 4 = (c ^ 2) ^ 2

Proof state:
⊢ FermatLastTheoremWith ℤ 4

Tactic:
intro a b c ha hb _ heq

Result:
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
a✝ : c ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 4
⊢ False
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem norm_cpow_of_imp {z w : ℂ} (h : z = 0 → w.re = 0 → w = 0) :
    ‖z ^ w‖ = ‖z‖ ^ w.re / Real.exp (arg z * im w)

Proof state:
case inr.inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re ≠ 0
⊢ ‖0 ^ w‖ = 0 ^ w.re / rexp (arg 0 * w.im)

Tactic:
rw [Real.zero_rpow hw, zero_div, zero_cpow, norm_zero]

Result:
case inr.inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re ≠ 0
⊢ w ≠ 0

Proof state:
z w : ℂ
h : z = 0 → w.re = 0 → w = 0
⊢ ‖z ^ w‖ = ‖z‖ ^ w.re / rexp (z.arg * w.im)

Tactic:
rcases ne_or_eq z 0 with (hz | rfl) <;> [exact norm_cpow_of_ne_zero hz w; rw [norm_zero]]

Result:
case inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
⊢ ‖0 ^ w‖ = 0 ^ w.re / rexp (arg 0 * w.im)

Proof state:
case inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
⊢ ‖0 ^ w‖ = 0 ^ w.re / rexp (arg 0 * w.im)

Tactic:
rcases eq_or_ne w.re 0 with hw | hw

Result:
case inr.inl
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re = 0
⊢ ‖0 ^ w‖ = 0 ^ w.re / rexp (arg 0 * w.im)

case inr.inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re ≠ 0
⊢ ‖0 ^ w‖ = 0 ^ w.re / rexp (arg 0 * w.im)

Proof state:
case inr.inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re ≠ 0
⊢ w ≠ 0

Tactic:
exact ne_of_apply_ne re hw

Result:
no goals

Proof state:
case inr.inl
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re = 0
⊢ ‖0 ^ w‖ = 0 ^ w.re / rexp (arg 0 * w.im)

Tactic:
simp [hw, h rfl hw]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
@[simp]
lemma DifferentiableOn.sub_iff_left (hg : DifferentiableOn 𝕜 g s) :
    DifferentiableOn 𝕜 (fun y => f y - g y) s ↔ DifferentiableOn 𝕜 f s

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
s : Set E
hg : DifferentiableOn 𝕜 g s
⊢ DifferentiableOn 𝕜 (fun y => f y - g y) s ↔ DifferentiableOn 𝕜 f s

Tactic:
simp only [sub_eq_add_neg, differentiableOn_neg_iff, hg, add_iff_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head?_append {l : List α} : (l ++ l').head? = l.head?.or l'.head?

Proof state:
α : Type u_1
l' l : List α
⊢ (l ++ l').head? = l.head?.or l'.head?

Tactic:
cases l <;> rfl

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Defs.lean
theorem factorization_pow (n k : ℕ) : factorization (n ^ k) = k • n.factorization

Proof state:
case zero
n : ℕ
⊢ (n ^ 0).factorization = 0 • n.factorization

Tactic:
simp

Result:
no goals

Proof state:
case succ
n k : ℕ
ih : (n ^ k).factorization = k • n.factorization
⊢ (n ^ (k + 1)).factorization = (k + 1) • n.factorization

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Result:
case succ.inl
k : ℕ
ih : (0 ^ k).factorization = k • factorization 0
⊢ (0 ^ (k + 1)).factorization = (k + 1) • factorization 0

case succ.inr
n k : ℕ
ih : (n ^ k).factorization = k • n.factorization
hn : n ≠ 0
⊢ (n ^ (k + 1)).factorization = (k + 1) • n.factorization

Proof state:
case succ.inl
k : ℕ
ih : (0 ^ k).factorization = k • factorization 0
⊢ (0 ^ (k + 1)).factorization = (k + 1) • factorization 0

Tactic:
simp

Result:
no goals

Proof state:
n k : ℕ
⊢ (n ^ k).factorization = k • n.factorization

Tactic:
induction' k with k ih

Result:
case zero
n : ℕ
⊢ (n ^ 0).factorization = 0 • n.factorization

case succ
n k : ℕ
ih : (n ^ k).factorization = k • n.factorization
⊢ (n ^ (k + 1)).factorization = (k + 1) • n.factorization

Proof state:
case succ.inr
n k : ℕ
ih : (n ^ k).factorization = k • n.factorization
hn : n ≠ 0
⊢ (n ^ (k + 1)).factorization = (k + 1) • n.factorization

Tactic:
rw [Nat.pow_succ, mul_comm, factorization_mul hn (pow_ne_zero _ hn), ih,
  add_smul, one_smul, add_comm]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem add_mul (φ₁ φ₂ φ₃ : MvPowerSeries σ R) : (φ₁ + φ₂) * φ₃ = φ₁ * φ₃ + φ₂ * φ₃ :=
  ext fun n => by
    classical simp only [coeff_mul, add_mul, Finset.sum_add_distrib, LinearMap.map_add]

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (coeff R n) ((φ₁ + φ₂) * φ₃) = (coeff R n) (φ₁ * φ₃ + φ₂ * φ₃)

Tactic:
simp only [coeff_mul, add_mul, Finset.sum_add_distrib, LinearMap.map_add]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (coeff R n) ((φ₁ + φ₂) * φ₃) = (coeff R n) (φ₁ * φ₃ + φ₂ * φ₃)

Tactic:
classical simp only [coeff_mul, add_mul, Finset.sum_add_distrib, LinearMap.map_add]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Lemmas.lean
theorem pow_left (H : IsRelPrime x y) : IsRelPrime (x ^ m) y

Proof state:
α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x y : α
m : ℕ
H : IsRelPrime x y
⊢ IsRelPrime (x ^ m) y

Tactic:
rw [← Finset.card_range m, ← Finset.prod_const]

Result:
α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x y : α
m : ℕ
H : IsRelPrime x y
⊢ IsRelPrime (∏ _x ∈ Finset.range m, x) y

Proof state:
α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x y : α
m : ℕ
H : IsRelPrime x y
⊢ IsRelPrime (∏ _x ∈ Finset.range m, x) y

Tactic:
exact IsRelPrime.prod_left fun _ _ ↦ H

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
lemma isIso_app_iff_of_iso {F G : C ⥤ D} (α : F ⟶ G) {X Y : C} (e : X ≅ Y) :
    IsIso (α.app X) ↔ IsIso (α.app Y) :=
  (MorphismProperty.isomorphisms D).arrow_mk_iso_iff
    (Arrow.isoMk (F.mapIso e) (G.mapIso e) (by simp))

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F G : C ⥤ D
α : F ⟶ G
X Y : C
e : X ≅ Y
⊢ (F.mapIso e).hom ≫ (Arrow.mk (α.app Y)).hom = (Arrow.mk (α.app X)).hom ≫ (G.mapIso e).hom

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Process/Stopping.lean
theorem IsStoppingTime.measurableSet_eq (hτ : IsStoppingTime f τ) (i : ι) :
    MeasurableSet[f i] {ω | τ ω = i}

Proof state:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
⊢ ω ∈ {ω | τ ω = i} ↔ ω ∈ {ω | τ ω ≤ i} ∩ {ω | τ ω ≥ i}

Tactic:
simp only [Set.mem_setOf_eq, Set.mem_inter_iff, le_antisymm_iff]

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ {ω | τ ω = i} = {ω | τ ω ≤ i} ∩ {ω | τ ω ≥ i}

Tactic:
ext1 ω

Result:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
⊢ ω ∈ {ω | τ ω = i} ↔ ω ∈ {ω | τ ω ≤ i} ∩ {ω | τ ω ≥ i}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | τ ω = i} = {ω | τ ω ≤ i} ∩ {ω | τ ω ≥ i}
⊢ MeasurableSet ({ω | τ ω ≤ i} ∩ {ω | τ ω ≥ i})

Tactic:
exact (hτ.measurableSet_le i).inter (hτ.measurableSet_ge i)

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet {ω | τ ω = i}

Tactic:
have : {ω | τ ω = i} = {ω | τ ω ≤ i} ∩ {ω | τ ω ≥ i} := by
  ext1 ω; simp only [Set.mem_setOf_eq, Set.mem_inter_iff, le_antisymm_iff]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | τ ω = i} = {ω | τ ω ≤ i} ∩ {ω | τ ω ≥ i}
⊢ MeasurableSet {ω | τ ω = i}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | τ ω = i} = {ω | τ ω ≤ i} ∩ {ω | τ ω ≥ i}
⊢ MeasurableSet {ω | τ ω = i}

Tactic:
rw [this]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | τ ω = i} = {ω | τ ω ≤ i} ∩ {ω | τ ω ≥ i}
⊢ MeasurableSet ({ω | τ ω ≤ i} ∩ {ω | τ ω ≥ i})
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem span_preimage_eq [RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {s : Set M₂} (h₀ : s.Nonempty)
    (h₁ : s ⊆ range f) : span R (f ⁻¹' s) = (span R₂ s).comap f

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ ↑(range f)
⊢ ker f ≤ span R (⇑f ⁻¹' s)

Tactic:
let y := Classical.choose h₀

Result:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ ↑(range f)
y : M₂ := Classical.choose h₀
⊢ ker f ≤ span R (⇑f ⁻¹' s)

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ ↑(range f)
hk : span R (⇑f ⁻¹' s) = span R (⇑f ⁻¹' s) ⊔ ker f
⊢ comap f (span R₂ s) ≤ span R (⇑f ⁻¹' s)

Tactic:
rw [range_coe f] at h₁

Result:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ Set.range ⇑f
hk : span R (⇑f ⁻¹' s) = span R (⇑f ⁻¹' s) ⊔ ker f
⊢ comap f (span R₂ s) ≤ span R (⇑f ⁻¹' s)

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ Set.range ⇑f
hk : span R (⇑f ⁻¹' s) = span R (⇑f ⁻¹' s) ⊔ ker f
⊢ range f ⊓ span R₂ s ≤ span R₂ s

Tactic:
exact inf_le_right

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem dlookup_kinsert_ne {a a'} {b' : β a'} {l : List (Sigma β)} (h : a ≠ a') :
    dlookup a (kinsert a' b' l) = dlookup a l

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : a ≠ a'
⊢ dlookup a (kinsert a' b' l) = dlookup a l

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive]
lemma subset_pow (hs : 1 ∈ s) (hn : n ≠ 0) : s ⊆ s ^ n

Proof state:
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
hs : 1 ∈ s
hn : n ≠ 0
⊢ s ⊆ s ^ n

Tactic:
simpa using pow_subset_pow_right hs <| Nat.one_le_iff_ne_zero.2 hn

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
lemma coproducts_of_small {X Y : C} (f : X ⟶ Y) {J : Type w'}
    (hf : W.colimitsOfShape (Discrete J) f) [Small.{w} J] :
    coproducts.{w} W f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
X Y : C
f : X ⟶ Y
J : Type w'
hf : W.colimitsOfShape (Discrete J) f
inst✝ : Small.{w, w'} J
⊢ coproducts.{w, v, u} W f

Tactic:
rw [coproducts_iff]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
X Y : C
f : X ⟶ Y
J : Type w'
hf : W.colimitsOfShape (Discrete J) f
inst✝ : Small.{w, w'} J
⊢ ∃ J, W.colimitsOfShape (Discrete J) f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
X Y : C
f : X ⟶ Y
J : Type w'
hf : W.colimitsOfShape (Discrete J) f
inst✝ : Small.{w, w'} J
⊢ ∃ J, W.colimitsOfShape (Discrete J) f

Tactic:
refine ⟨Shrink J, ?_⟩

Result:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
X Y : C
f : X ⟶ Y
J : Type w'
hf : W.colimitsOfShape (Discrete J) f
inst✝ : Small.{w, w'} J
⊢ W.colimitsOfShape (Discrete (Shrink.{w, w'} J)) f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
X Y : C
f : X ⟶ Y
J : Type w'
hf : W.colimitsOfShape (Discrete J) f
inst✝ : Small.{w, w'} J
⊢ W.colimitsOfShape (Discrete (Shrink.{w, w'} J)) f

Tactic:
rwa [← W.colimitsOfShape_eq_of_equivalence (Discrete.equivalence (equivShrink.{w} J))]

Result:
no goals