harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Compactness/Compact.lean
theorem Filter.coprodᵢ_cocompact {X : ι → Type*} [∀ d, TopologicalSpace (X d)] :
    (Filter.coprodᵢ fun d => Filter.cocompact (X d)) = Filter.cocompact (∀ d, X d)

Proof state:
ι : Type u_1
X : ι → Type u_3
inst✝ : (d : ι) → TopologicalSpace (X d)
s : Set ((i : ι) → X i)
K : (i : ι) → Set (X i)
hKc : ∀ (i : ι), IsCompact (K i)
htK : ∀ (i : ι), s ⊆ eval i ⁻¹' K i
⊢ ∃ t, IsCompact t ∧ s ⊆ t

Tactic:
exact ⟨Set.pi univ K, isCompact_univ_pi hKc, fun f hf i _ => htK i hf⟩

Result:
no goals

Proof state:
ι : Type u_1
X : ι → Type u_3
inst✝ : (d : ι) → TopologicalSpace (X d)
⊢ cocompact ((d : ι) → X d) ≤ Filter.coprodᵢ fun d => cocompact (X d)

Tactic:
refine compl_surjective.forall.2 fun s H => ?_

Result:
ι : Type u_1
X : ι → Type u_3
inst✝ : (d : ι) → TopologicalSpace (X d)
s : Set ((i : ι) → X i)
H : sᶜ ∈ Filter.coprodᵢ fun d => cocompact (X d)
⊢ sᶜ ∈ cocompact ((d : ι) → X d)

Proof state:
ι : Type u_1
X : ι → Type u_3
inst✝ : (d : ι) → TopologicalSpace (X d)
s : Set ((i : ι) → X i)
H : sᶜ ∈ Filter.coprodᵢ fun d => cocompact (X d)
⊢ sᶜ ∈ cocompact ((d : ι) → X d)

Tactic:
simp only [compl_mem_coprodᵢ, Filter.mem_cocompact, compl_subset_compl, image_subset_iff] at H ⊢

Result:
ι : Type u_1
X : ι → Type u_3
inst✝ : (d : ι) → TopologicalSpace (X d)
s : Set ((i : ι) → X i)
H : ∀ (i : ι), ∃ t, IsCompact t ∧ s ⊆ eval i ⁻¹' t
⊢ ∃ t, IsCompact t ∧ s ⊆ t

Proof state:
ι : Type u_1
X : ι → Type u_3
inst✝ : (d : ι) → TopologicalSpace (X d)
⊢ (Filter.coprodᵢ fun d => cocompact (X d)) = cocompact ((d : ι) → X d)

Tactic:
refine le_antisymm (iSup_le fun i => Filter.comap_cocompact_le (continuous_apply i)) ?_

Result:
ι : Type u_1
X : ι → Type u_3
inst✝ : (d : ι) → TopologicalSpace (X d)
⊢ cocompact ((d : ι) → X d) ≤ Filter.coprodᵢ fun d => cocompact (X d)

Proof state:
ι : Type u_1
X : ι → Type u_3
inst✝ : (d : ι) → TopologicalSpace (X d)
s : Set ((i : ι) → X i)
H : ∀ (i : ι), ∃ t, IsCompact t ∧ s ⊆ eval i ⁻¹' t
⊢ ∃ t, IsCompact t ∧ s ⊆ t

Tactic:
choose K hKc htK using H

Result:
ι : Type u_1
X : ι → Type u_3
inst✝ : (d : ι) → TopologicalSpace (X d)
s : Set ((i : ι) → X i)
K : (i : ι) → Set (X i)
hKc : ∀ (i : ι), IsCompact (K i)
htK : ∀ (i : ι), s ⊆ eval i ⁻¹' K i
⊢ ∃ t, IsCompact t ∧ s ⊆ t
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem wellPowered_of_isDetecting [HasPullbacks C] {𝒢 : Set C} [Small.{w} 𝒢]
    [LocallySmall.{w} C] (h𝒢 : IsDetecting 𝒢) : WellPowered.{w} C :=
  ⟨fun X =>
    @small_of_injective _ _ _ (fun P : Subobject X => { f : ΣG : 𝒢, G.1 ⟶ X | P.Factors f.2 })
      fun P Q h => Subobject.eq_of_isDetecting h𝒢 _ _
        (by simpa [Set.ext_iff, Sigma.forall] using h)⟩

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasPullbacks C
𝒢 : Set C
inst✝¹ : Small.{w, u₁} ↑𝒢
inst✝ : LocallySmall.{w, v₁, u₁} C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h : (fun P => {f | P.Factors f.snd}) P = (fun P => {f | P.Factors f.snd}) Q
⊢ ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, P.Factors f ↔ Q.Factors f

Tactic:
simpa [Set.ext_iff, Sigma.forall] using h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem replicate_inj : replicate n a = replicate m b ↔ n = m ∧ (n = 0 ∨ a = b) :=
  ⟨fun h => have eq : n = m

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
b : α✝
h : replicate n a = replicate m b
⊢ n = m

Tactic:
simpa using congrArg length h

Result:
no goals

Proof state:
n : Nat
α✝ : Type u_1
a b : α✝
h : replicate n a = replicate n b
w : ¬n = 0
p : (fun x => x[0]?) (replicate n a) = (fun x => x[0]?) (replicate n b)
⊢ 0 < n

Tactic:
exact zero_lt_of_ne_zero w

Result:
no goals

Proof state:
case pos
n : Nat
α✝ : Type u_1
a b : α✝
h : replicate n a = replicate n b
w : n = 0
⊢ n = 0 ∨ a = b

Tactic:
simp_all

Result:
no goals

Proof state:
case neg.h
n : Nat
α✝ : Type u_1
a b : α✝
h : replicate n a = replicate n b
w : ¬n = 0
p : (fun x => x[0]?) (replicate n a) = (fun x => x[0]?) (replicate n b)
⊢ a = b

Tactic:
replace w : 0 < n := by exact zero_lt_of_ne_zero w

Result:
case neg.h
n : Nat
α✝ : Type u_1
a b : α✝
h : replicate n a = replicate n b
p : (fun x => x[0]?) (replicate n a) = (fun x => x[0]?) (replicate n b)
w : 0 < n
⊢ a = b

Proof state:
n : Nat
α✝ : Type u_1
a b : α✝
h : replicate n a = replicate n b
⊢ n = 0 ∨ a = b

Tactic:
by_cases w : n = 0

Result:
case pos
n : Nat
α✝ : Type u_1
a b : α✝
h : replicate n a = replicate n b
w : n = 0
⊢ n = 0 ∨ a = b

case neg
n : Nat
α✝ : Type u_1
a b : α✝
h : replicate n a = replicate n b
w : ¬n = 0
⊢ n = 0 ∨ a = b

Proof state:
case neg
n : Nat
α✝ : Type u_1
a b : α✝
h : replicate n a = replicate n b
w : ¬n = 0
⊢ n = 0 ∨ a = b

Tactic:
right

Result:
case neg.h
n : Nat
α✝ : Type u_1
a b : α✝
h : replicate n a = replicate n b
w : ¬n = 0
⊢ a = b

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
b : α✝
h : replicate n a = replicate m b
eq : n = m
⊢ n = 0 ∨ a = b

Tactic:
subst eq

Result:
n : Nat
α✝ : Type u_1
a b : α✝
h : replicate n a = replicate n b
⊢ n = 0 ∨ a = b

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
b : α✝
⊢ n = m ∧ (n = 0 ∨ a = b) → replicate n a = replicate m b

Tactic:
rintro ⟨rfl, rfl | rfl⟩ <;> rfl

Result:
no goals

Proof state:
case neg.h
n : Nat
α✝ : Type u_1
a b : α✝
h : replicate n a = replicate n b
p : (fun x => x[0]?) (replicate n a) = (fun x => x[0]?) (replicate n b)
w : 0 < n
⊢ a = b

Tactic:
simp only [getElem?_replicate, if_pos w] at p

Result:
case neg.h
n : Nat
α✝ : Type u_1
a b : α✝
h : replicate n a = replicate n b
w : 0 < n
p : some a = some b
⊢ a = b

Proof state:
case neg.h
n : Nat
α✝ : Type u_1
a b : α✝
h : replicate n a = replicate n b
w : 0 < n
p : some a = some b
⊢ a = b

Tactic:
simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem sublist_eraseKey [BEq α] {l : List ((a : α) × β a)} {k : α} :
    Sublist (eraseKey k l) l

Proof state:
case false
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
t : List ((a : α) × β a)
ih : (eraseKey k t).Sublist t
⊢ (bif false then t else ⟨k', v'⟩ :: eraseKey k t).Sublist (⟨k', v'⟩ :: t)

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
⊢ (eraseKey k l).Sublist l

Tactic:
induction l using assoc_induction

Result:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
k : α
⊢ (eraseKey k []).Sublist []

case cons
α : Type u
β : α → Type v
inst✝ : BEq α
k k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ : (eraseKey k tail✝).Sublist tail✝
⊢ (eraseKey k (⟨k✝, v✝⟩ :: tail✝)).Sublist (⟨k✝, v✝⟩ :: tail✝)

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
k : α
⊢ (eraseKey k []).Sublist []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
t : List ((a : α) × β a)
ih : (eraseKey k t).Sublist t
⊢ (eraseKey k (⟨k', v'⟩ :: t)).Sublist (⟨k', v'⟩ :: t)

Tactic:
rw [eraseKey_cons]

Result:
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
t : List ((a : α) × β a)
ih : (eraseKey k t).Sublist t
⊢ (bif k' == k then t else ⟨k', v'⟩ :: eraseKey k t).Sublist (⟨k', v'⟩ :: t)

Proof state:
case true
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
t : List ((a : α) × β a)
ih : (eraseKey k t).Sublist t
⊢ (bif true then t else ⟨k', v'⟩ :: eraseKey k t).Sublist (⟨k', v'⟩ :: t)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
t : List ((a : α) × β a)
ih : (eraseKey k t).Sublist t
⊢ (bif k' == k then t else ⟨k', v'⟩ :: eraseKey k t).Sublist (⟨k', v'⟩ :: t)

Tactic:
cases k' == k

Result:
case false
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
t : List ((a : α) × β a)
ih : (eraseKey k t).Sublist t
⊢ (bif false then t else ⟨k', v'⟩ :: eraseKey k t).Sublist (⟨k', v'⟩ :: t)

case true
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
t : List ((a : α) × β a)
ih : (eraseKey k t).Sublist t
⊢ (bif true then t else ⟨k', v'⟩ :: eraseKey k t).Sublist (⟨k', v'⟩ :: t)
-- Mathlib/Data/Fin/Tuple/Finset.lean
lemma map_snocEquiv_filter_piFinset (P : (∀ i, α (castSucc i)) → Prop) [DecidablePred P] :
    {r ∈ piFinset S | P (init r)}.map (snocEquiv α).symm.toEmbedding =
      S (last _) ×ˢ {r ∈ piFinset (init S) | P r}

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.castSucc) → Prop
inst✝ : DecidablePred P
⊢ map (snocEquiv α).symm.toEmbedding (filter (fun r => P (init r)) (piFinset S)) =
    S (last n) ×ˢ filter (fun r => P r) (piFinset (init S))

Tactic:
unfold init

Result:
n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.castSucc) → Prop
inst✝ : DecidablePred P
⊢ map (snocEquiv α).symm.toEmbedding (filter (fun r => P fun i => r i.castSucc) (piFinset S)) =
    S (last n) ×ˢ filter (fun r => P r) (piFinset fun i => S i.castSucc)

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.castSucc) → Prop
inst✝ : DecidablePred P
⊢ map (snocEquiv α).symm.toEmbedding (filter (fun r => P fun i => r i.castSucc) (piFinset S)) =
    S (last n) ×ˢ filter (fun r => P r) (piFinset fun i => S i.castSucc)

Tactic:
ext

Result:
case h
n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.castSucc) → Prop
inst✝ : DecidablePred P
a✝ : α (last n) × ((i : Fin n) → α i.castSucc)
⊢ a✝ ∈ map (snocEquiv α).symm.toEmbedding (filter (fun r => P fun i => r i.castSucc) (piFinset S)) ↔
    a✝ ∈ S (last n) ×ˢ filter (fun r => P r) (piFinset fun i => S i.castSucc)

Proof state:
case h
n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.castSucc) → Prop
inst✝ : DecidablePred P
a✝ : α (last n) × ((i : Fin n) → α i.castSucc)
⊢ a✝ ∈ map (snocEquiv α).symm.toEmbedding (filter (fun r => P fun i => r i.castSucc) (piFinset S)) ↔
    a✝ ∈ S (last n) ×ˢ filter (fun r => P r) (piFinset fun i => S i.castSucc)

Tactic:
simp [Fin.forall_iff_castSucc, and_assoc]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem coe_lieSpan_submodule_eq_iff {p : Submodule R M} :
    (lieSpan R L (p : Set M) : Submodule R M) = p ↔ ∃ N : LieSubmodule R L M, ↑N = p

Proof state:
case mp
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
h : ↑(lieSpan R L ↑p) = p
⊢ ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p

Tactic:
intro x m hm

Result:
case mp
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
h : ↑(lieSpan R L ↑p) = p
x : L
m : M
hm : m ∈ p
⊢ ⁅x, m⁆ ∈ p

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
⊢ ↑(lieSpan R L ↑p) = p ↔ ∃ N, ↑N = p

Tactic:
rw [p.exists_lieSubmodule_coe_eq_iff L]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
⊢ ↑(lieSpan R L ↑p) = p ↔ ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p

Proof state:
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
h : ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p
⊢ ↑(lieSpan R L ↑p) = p

Tactic:
rw [← toSubmodule_mk p @h, coe_toSubmodule, toSubmodule_inj, lieSpan_eq]

Result:
no goals

Proof state:
case mp
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
h : ↑(lieSpan R L ↑p) = p
x : L
m : M
hm : m ∈ p
⊢ ⁅x, m⁆ ∈ lieSpan R L ↑p

Tactic:
exact lie_mem _ (subset_lieSpan hm)

Result:
no goals

Proof state:
case mp
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
h : ↑(lieSpan R L ↑p) = p
x : L
m : M
hm : m ∈ p
⊢ ⁅x, m⁆ ∈ p

Tactic:
rw [← h, mem_toSubmodule]

Result:
case mp
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
h : ↑(lieSpan R L ↑p) = p
x : L
m : M
hm : m ∈ p
⊢ ⁅x, m⁆ ∈ lieSpan R L ↑p

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
⊢ ↑(lieSpan R L ↑p) = p ↔ ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p

Tactic:
constructor <;> intro h

Result:
case mp
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
h : ↑(lieSpan R L ↑p) = p
⊢ ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p

case mpr
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
h : ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p
⊢ ↑(lieSpan R L ↑p) = p
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_eq_nhds_of_re_neg_of_im_pos (hx_re : x.re < 0) (hx_im : 0 < x.im) :
    arg =ᶠ[𝓝 x] fun x => Real.arcsin ((-x).im / ‖x‖) + π

Proof state:
x : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
⊢ arg =ᶠ[𝓝 x] fun x => Real.arcsin ((-x).im / ‖x‖) + π

Tactic:
suffices h_forall_nhds : ∀ᶠ y : ℂ in 𝓝 x, y.re < 0 ∧ 0 < y.im from
  h_forall_nhds.mono fun y hy => arg_of_re_neg_of_im_nonneg hy.1 hy.2.le

Result:
x : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
⊢ ∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ 0 < y.im

Proof state:
x : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
⊢ IsOpen fun y => y.re < 0 ∧ 0 < y.im

Tactic:
exact
  IsOpen.and (isOpen_lt continuous_re continuous_zero) (isOpen_lt continuous_zero continuous_im)

Result:
no goals

Proof state:
x : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
⊢ ∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ 0 < y.im

Tactic:
refine IsOpen.eventually_mem ?_ (⟨hx_re, hx_im⟩ : x.re < 0 ∧ 0 < x.im)

Result:
x : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
⊢ IsOpen fun y => y.re < 0 ∧ 0 < y.im
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem b₆_of_isCharTwoJNeZeroNF_of_char_two : W.b₆ = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ 4 * W.a₆ = 0

Tactic:
linear_combination 2 * W.a₆ * CharP.cast_eq_zero R 2

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ W.b₆ = 0

Tactic:
rw [b₆_of_isCharTwoJNeZeroNF]

Result:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ 4 * W.a₆ = 0
-- Mathlib/Analysis/Normed/Group/NullSubmodule.lean
@[to_additive]
lemma isClosed_nullSubgroup : IsClosed (nullSubgroup M : Set M)

Proof state:
M : Type u_1
inst✝ : SeminormedCommGroup M
⊢ IsClosed ↑(nullSubgroup M)

Tactic:
apply isClosed_singleton.preimage continuous_norm'

Result:
no goals
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem yn_modEq_a_sub_one : ∀ n, yn a1 n ≡ n [MOD a - 1]
  | 0 => by simp [Nat.ModEq.refl]
  | 1 => by simp [Nat.ModEq.refl]
  | n + 2 =>
    (yn_modEq_a_sub_one n).add_right_cancel <| by
      rw [yn_succ_succ, (by ring : n + 2 + n = 2 * (n + 1))]
      exact ((modEq_sub a1.le).mul_left 2).mul (yn_modEq_a_sub_one (n + 1))

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ n + 2 + n = 2 * (n + 1)

Tactic:
ring

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ yn a1 (n + 2) + yn a1 n ≡ n + 2 + n [MOD a - 1]

Tactic:
rw [yn_succ_succ, (by ring : n + 2 + n = 2 * (n + 1))]

Result:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ 2 * a * yn a1 (n + 1) ≡ 2 * (n + 1) [MOD a - 1]

Proof state:
a : ℕ
a1 : 1 < a
⊢ yn a1 1 ≡ 1 [MOD a - 1]

Tactic:
simp [Nat.ModEq.refl]

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
⊢ yn a1 0 ≡ 0 [MOD a - 1]

Tactic:
simp [Nat.ModEq.refl]

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ 2 * a * yn a1 (n + 1) ≡ 2 * (n + 1) [MOD a - 1]

Tactic:
exact ((modEq_sub a1.le).mul_left 2).mul (yn_modEq_a_sub_one (n + 1))

Result:
no goals
-- Mathlib/Algebra/Star/Subalgebra.lean
theorem toSubalgebra_injective :
    Function.Injective (toSubalgebra : StarSubalgebra R A → Subalgebra R A) := fun S T h =>
  ext fun x => by rw [← mem_toSubalgebra, ← mem_toSubalgebra, h]

Proof state:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
S T : StarSubalgebra R A
h : S.toSubalgebra = T.toSubalgebra
x : A
⊢ x ∈ S ↔ x ∈ T

Tactic:
rw [← mem_toSubalgebra, ← mem_toSubalgebra, h]

Result:
no goals
-- Mathlib/Data/List/Dedup.lean
theorem mem_dedup {a : α} {l : List α} : a ∈ dedup l ↔ a ∈ l

Proof state:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ ∀ {x y z : α}, (fun x1 x2 => x1 ≠ x2) x z → (fun x1 x2 => x1 ≠ x2) x y ∨ (fun x1 x2 => x1 ≠ x2) y z

Tactic:
intros x y z xz

Result:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
x y z : α
xz : x ≠ z
⊢ (fun x1 x2 => x1 ≠ x2) x y ∨ (fun x1 x2 => x1 ≠ x2) y z

Proof state:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
this : (¬∀ b ∈ pwFilter (fun x1 x2 => x1 ≠ x2) l, a ≠ b) ↔ ¬∀ b ∈ l, a ≠ b
⊢ a ∈ l.dedup ↔ a ∈ l

Tactic:
simpa only [dedup, forall_mem_ne, not_not] using this

Result:
no goals

Proof state:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
x y z : α
xz : x ≠ z
⊢ (fun x1 x2 => x1 ≠ x2) x y ∨ (fun x1 x2 => x1 ≠ x2) y z

Tactic:
exact not_and_or.1 <| mt (fun h ↦ h.1.trans h.2) xz

Result:
no goals
-- Mathlib/CategoryTheory/Grothendieck.lean
theorem fiber_eqToHom {X Y : Grothendieck F} (h : X = Y) :
    (eqToHom h).fiber = eqToHom (by subst h; simp)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X : Grothendieck F
⊢ (F.map (eqToHom ⋯).base).obj X.fiber = X.fiber

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
h : X = Y
⊢ (eqToHom h).fiber = eqToHom ⋯

Tactic:
subst h

Result:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X : Grothendieck F
⊢ (eqToHom ⋯).fiber = eqToHom ⋯

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X : Grothendieck F
⊢ (eqToHom ⋯).fiber = eqToHom ⋯

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
h : X = Y
⊢ (F.map (eqToHom h).base).obj X.fiber = Y.fiber

Tactic:
subst h

Result:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X : Grothendieck F
⊢ (F.map (eqToHom ⋯).base).obj X.fiber = X.fiber
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem linkAux_size : (linkAux self x y).size = self.size

Proof state:
self : Array UFNode
x y : Fin self.size
⊢ (linkAux self x y).size = self.size

Tactic:
simp only [linkAux, Array.get_eq_getElem]

Result:
self : Array UFNode
x y : Fin self.size
⊢ (if ↑x = ↑y then self
      else
        if self[↑y].rank < self[↑x].rank then self.set ↑y { parent := ↑x, rank := self[↑y].rank } ⋯
        else
          if self[↑x].rank = self[↑y].rank then
            (self.set ↑x { parent := ↑y, rank := self[↑x].rank } ⋯).set ↑y
              { parent := self[↑y].parent, rank := self[↑y].rank + 1 } ⋯
          else self.set ↑x { parent := ↑y, rank := self[↑x].rank } ⋯).size =
    self.size

Proof state:
self : Array UFNode
x y : Fin self.size
⊢ (if ↑x = ↑y then self
      else
        if self[↑y].rank < self[↑x].rank then self.set ↑y { parent := ↑x, rank := self[↑y].rank } ⋯
        else
          if self[↑x].rank = self[↑y].rank then
            (self.set ↑x { parent := ↑y, rank := self[↑x].rank } ⋯).set ↑y
              { parent := self[↑y].parent, rank := self[↑y].rank + 1 } ⋯
          else self.set ↑x { parent := ↑y, rank := self[↑x].rank } ⋯).size =
    self.size

Tactic:
split <;> [rfl; split] <;> [skip; split] <;> simp

Result:
no goals
-- Mathlib/RingTheory/Norm/Transitivity.lean
/-- The lower-right corner of `M * aux M k` is the same as the corner of `M`. -/
lemma mul_auxMat_corner : (M * auxMat M k) k k = M k k

Proof state:
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
⊢ (M * auxMat M k) k k = M k k

Tactic:
simp [Matrix.mul_apply, auxMat]

Result:
no goals
-- Mathlib/Algebra/Group/Semiconj/Defs.lean
theorem mul_left (ha : SemiconjBy a y z) (hb : SemiconjBy b x y) : SemiconjBy (a * b) x z

Proof state:
S : Type u_1
inst✝ : Semigroup S
a b x y z : S
ha : SemiconjBy a y z
hb : SemiconjBy b x y
⊢ a * b * x = z * (a * b)

Tactic:
rw [mul_assoc, hb.eq, ← mul_assoc, ha.eq, mul_assoc]

Result:
no goals

Proof state:
S : Type u_1
inst✝ : Semigroup S
a b x y z : S
ha : SemiconjBy a y z
hb : SemiconjBy b x y
⊢ SemiconjBy (a * b) x z

Tactic:
unfold SemiconjBy

Result:
S : Type u_1
inst✝ : Semigroup S
a b x y z : S
ha : SemiconjBy a y z
hb : SemiconjBy b x y
⊢ a * b * x = z * (a * b)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Gcd.lean
theorem gcd_dvd (m n : Nat) : (gcd m n ∣ m) ∧ (gcd m n ∣ n)

Proof state:
case H1
m n : Nat
a✝ : 0 < m
IH : m.gcd n ∣ n % m ∧ m.gcd n ∣ m
⊢ m.gcd n ∣ m ∧ m.gcd n ∣ n

Tactic:
exact ⟨IH.2, (dvd_mod_iff IH.2).1 IH.1⟩

Result:
no goals

Proof state:
case H1
m n : Nat
a✝ : 0 < m
IH : (n % m).gcd m ∣ n % m ∧ (n % m).gcd m ∣ m
⊢ m.gcd n ∣ m ∧ m.gcd n ∣ n

Tactic:
rw [← gcd_rec] at IH

Result:
case H1
m n : Nat
a✝ : 0 < m
IH : m.gcd n ∣ n % m ∧ m.gcd n ∣ m
⊢ m.gcd n ∣ m ∧ m.gcd n ∣ n

Proof state:
case H0
n : Nat
⊢ n ∣ 0 ∧ n ∣ n

Tactic:
exact ⟨Nat.dvd_zero n, Nat.dvd_refl n⟩

Result:
no goals

Proof state:
case H0
n : Nat
⊢ gcd 0 n ∣ 0 ∧ gcd 0 n ∣ n

Tactic:
rw [gcd_zero_left]

Result:
case H0
n : Nat
⊢ n ∣ 0 ∧ n ∣ n

Proof state:
m n : Nat
⊢ m.gcd n ∣ m ∧ m.gcd n ∣ n

Tactic:
induction m, n using gcd.induction with
| H0 n => rw [gcd_zero_left]; exact ⟨Nat.dvd_zero n, Nat.dvd_refl n⟩
| H1 m n _ IH => rw [← gcd_rec] at IH; exact ⟨IH.2, (dvd_mod_iff IH.2).1 IH.1⟩

Result:
no goals
-- Mathlib/RingTheory/Localization/Basic.lean
theorem algHom_subsingleton [Algebra R P] : Subsingleton (S →ₐ[R] P) :=
  ⟨fun f g =>
    AlgHom.coe_ringHom_injective <|
      IsLocalization.ringHom_ext M <| by rw [f.comp_algebraMap, g.comp_algebraMap]⟩

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : IsLocalization M S
inst✝ : Algebra R P
f g : S →ₐ[R] P
⊢ (↑f).comp (algebraMap R S) = (↑g).comp (algebraMap R S)

Tactic:
rw [f.comp_algebraMap, g.comp_algebraMap]

Result:
no goals