internlm/Lean-Github huggingface dataset:
Theorem: sb_surjective
Proof state before:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
y : β
gyA : g y ∉ A
⊢ invFun g (g y) = y
Tactic:
apply leftInverse_invFun hg
Proof state after:
no goals
Theorem: sb_surjective
Proof state before:
case pos
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
y : β
gyA : g y ∈ A
⊢ ∃ a, h a = y
Tactic:
rw [A_def, sbSet, mem_iUnion] at gyA
Proof state after:
case pos
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
y : β
gyA : ∃ i, g y ∈ sbAux f g i
⊢ ∃ a, h a = y
Theorem: sb_surjective
Proof state before:
case pos
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
y : β
gyA : ∃ i, g y ∈ sbAux f g i
⊢ ∃ a, h a = y
Tactic:
rcases gyA with ⟨n, hn⟩
Proof state after:
case pos.intro
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
y : β
n : ℕ
hn : g y ∈ sbAux f g n
⊢ ∃ a, h a = y
Theorem: sb_surjective
Proof state before:
case pos.intro
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
y : β
n : ℕ
hn : g y ∈ sbAux f g n
⊢ ∃ a, h a = y
Tactic:
rcases n with _ | n
Proof state after:
case pos.intro.zero
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
y : β
hn : g y ∈ sbAux f g 0
⊢ ∃ a, h a = y

case pos.intro.succ
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
y : β
n : ℕ
hn : g y ∈ sbAux f g (n + 1)
⊢ ∃ a, h a = y
Theorem: sb_surjective
Proof state before:
case pos.intro.succ
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
y : β
n : ℕ
hn : g y ∈ sbAux f g (n + 1)
⊢ ∃ a, h a = y
Tactic:
simp [sbAux] at hn
Proof state after:
case pos.intro.succ
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
y : β
n : ℕ
hn : ∃ a ∈ sbAux f g n, g (f a) = g y
⊢ ∃ a, h a = y
Theorem: sb_surjective
Proof state before:
case pos.intro.succ
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
y : β
n : ℕ
hn : ∃ a ∈ sbAux f g n, g (f a) = g y
⊢ ∃ a, h a = y
Tactic:
rcases hn with ⟨x, xmem, hx⟩
Proof state after:
case pos.intro.succ.intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
y : β
n : ℕ
x : α
xmem : x ∈ sbAux f g n
hx : g (f x) = g y
⊢ ∃ a, h a = y
Theorem: sb_surjective
Proof state before:
case pos.intro.succ.intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
y : β
n : ℕ
x : α
xmem : x ∈ sbAux f g n
hx : g (f x) = g y
⊢ ∃ a, h a = y
Tactic:
use x
Proof state after:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
y : β
n : ℕ
x : α
xmem : x ∈ sbAux f g n
hx : g (f x) = g y
⊢ h x = y
Theorem: sb_surjective
Proof state before:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
y : β
n : ℕ
x : α
xmem : x ∈ sbAux f g n
hx : g (f x) = g y
⊢ h x = y
Tactic:
have : x ∈ A := by
  rw [A_def, sbSet, mem_iUnion]
  exact ⟨n, xmem⟩
Proof state after:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
y : β
n : ℕ
x : α
xmem : x ∈ sbAux f g n
hx : g (f x) = g y
this : x ∈ A
⊢ h x = y
Theorem: sb_surjective
Proof state before:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
y : β
n : ℕ
x : α
xmem : x ∈ sbAux f g n
hx : g (f x) = g y
this : x ∈ A
⊢ h x = y
Tactic:
simp only [h_def, sbFun, if_pos this]
Proof state after:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
y : β
n : ℕ
x : α
xmem : x ∈ sbAux f g n
hx : g (f x) = g y
this : x ∈ A
⊢ f x = y
Theorem: sb_surjective
Proof state before:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
y : β
n : ℕ
x : α
xmem : x ∈ sbAux f g n
hx : g (f x) = g y
this : x ∈ A
⊢ f x = y
Tactic:
exact hg hx
Proof state after:
no goals
Theorem: sb_surjective
Proof state before:
case pos.intro.zero
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
y : β
hn : g y ∈ sbAux f g 0
⊢ ∃ a, h a = y
Tactic:
simp [sbAux] at hn
Proof state after:
no goals
Theorem: sb_surjective
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
y : β
n : ℕ
x : α
xmem : x ∈ sbAux f g n
hx : g (f x) = g y
⊢ x ∈ A
Tactic:
rw [A_def, sbSet, mem_iUnion]
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
y : β
n : ℕ
x : α
xmem : x ∈ sbAux f g n
hx : g (f x) = g y
⊢ ∃ i, x ∈ sbAux f g i
Theorem: sb_surjective
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
y : β
n : ℕ
x : α
xmem : x ∈ sbAux f g n
hx : g (f x) = g y
⊢ ∃ i, x ∈ sbAux f g i
Tactic:
exact ⟨n, xmem⟩
Proof state after:
no goals
Theorem: even_of_even_sqr
Proof state before:
m : ℕ
h : 2 ∣ m ^ 2
⊢ 2 ∣ m
Tactic:
rw [pow_two, Nat.prime_two.dvd_mul] at h
Proof state after:
m : ℕ
h : 2 ∣ m ∨ 2 ∣ m
⊢ 2 ∣ m
Theorem: even_of_even_sqr
Proof state before:
m : ℕ
h : 2 ∣ m ∨ 2 ∣ m
⊢ 2 ∣ m
Tactic:
cases h <;> assumption
Proof state after:
no goals
Theorem: factorization_mul'
Proof state before:
m n : ℕ
mnez : m ≠ 0
nnez : n ≠ 0
p : ℕ
⊢ (m * n).factorization p = m.factorization p + n.factorization p
Tactic:
rw [Nat.factorization_mul mnez nnez]
Proof state after:
m n : ℕ
mnez : m ≠ 0
nnez : n ≠ 0
p : ℕ
⊢ (m.factorization + n.factorization) p = m.factorization p + n.factorization p
Theorem: factorization_mul'
Proof state before:
m n : ℕ
mnez : m ≠ 0
nnez : n ≠ 0
p : ℕ
⊢ (m.factorization + n.factorization) p = m.factorization p + n.factorization p
Tactic:
rfl
Proof state after:
no goals
Theorem: factorization_pow'
Proof state before:
n k p : ℕ
⊢ (n ^ k).factorization p = k * n.factorization p
Tactic:
rw [Nat.factorization_pow]
Proof state after:
n k p : ℕ
⊢ (k • n.factorization) p = k * n.factorization p
Theorem: factorization_pow'
Proof state before:
n k p : ℕ
⊢ (k • n.factorization) p = k * n.factorization p
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.Prime.factorization'
Proof state before:
p : ℕ
prime_p : p.Prime
⊢ p.factorization p = 1
Tactic:
rw [prime_p.factorization]
Proof state after:
p : ℕ
prime_p : p.Prime
⊢ (Finsupp.single p 1) p = 1
Theorem: Nat.Prime.factorization'
Proof state before:
p : ℕ
prime_p : p.Prime
⊢ (Finsupp.single p 1) p = 1
Tactic:
simp
Proof state after:
no goals
Theorem: cauchySeq_of_le_geometric_two'
Proof state before:
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
⊢ CauchySeq u
Tactic:
rw [Metric.cauchySeq_iff']
Proof state after:
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) (u N) < ε
Theorem: cauchySeq_of_le_geometric_two'
Proof state before:
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) (u N) < ε
Tactic:
intro ε ε_pos
Proof state after:
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, ∀ n ≥ N, dist (u n) (u N) < ε
Theorem: cauchySeq_of_le_geometric_two'
Proof state before:
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, ∀ n ≥ N, dist (u n) (u N) < ε
Tactic:
obtain ⟨N, hN⟩ : ∃ N : ℕ, 1 / 2 ^ N * 2 < ε := by sorry
Proof state after:
case intro
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : 1 / 2 ^ N * 2 < ε
⊢ ∃ N, ∀ n ≥ N, dist (u n) (u N) < ε
Theorem: cauchySeq_of_le_geometric_two'
Proof state before:
case intro
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : 1 / 2 ^ N * 2 < ε
⊢ ∃ N, ∀ n ≥ N, dist (u n) (u N) < ε
Tactic:
use N
Proof state after:
case h
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : 1 / 2 ^ N * 2 < ε
⊢ ∀ n ≥ N, dist (u n) (u N) < ε
Theorem: cauchySeq_of_le_geometric_two'
Proof state before:
case h
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : 1 / 2 ^ N * 2 < ε
⊢ ∀ n ≥ N, dist (u n) (u N) < ε
Tactic:
intro n hn
Proof state after:
case h
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : 1 / 2 ^ N * 2 < ε
n : ℕ
hn : n ≥ N
⊢ dist (u n) (u N) < ε
Theorem: cauchySeq_of_le_geometric_two'
Proof state before:
case h
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : 1 / 2 ^ N * 2 < ε
n : ℕ
hn : n ≥ N
⊢ dist (u n) (u N) < ε
Tactic:
obtain ⟨k, rfl : n = N + k⟩ := le_iff_exists_add.mp hn
Proof state after:
case h.intro
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : 1 / 2 ^ N * 2 < ε
k : ℕ
hn : N + k ≥ N
⊢ dist (u (N + k)) (u N) < ε
Theorem: cauchySeq_of_le_geometric_two'
Proof state before:
case h.intro
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : 1 / 2 ^ N * 2 < ε
k : ℕ
hn : N + k ≥ N
⊢ dist (u (N + k)) (u N) < ε
Tactic:
calc
  dist (u (N + k)) (u N) = dist (u (N + 0)) (u (N + k)) := sorry
  _ ≤ ∑ i in range k, dist (u (N + i)) (u (N + (i + 1))) := sorry
  _ ≤ ∑ i in range k, (1 / 2 : ℝ) ^ (N + i) := sorry
  _ = 1 / 2 ^ N * ∑ i in range k, (1 / 2 : ℝ) ^ i := sorry
  _ ≤ 1 / 2 ^ N * 2 := sorry
  _ < ε := sorry
Proof state after:
no goals
Theorem: cauchySeq_of_le_geometric_two'
Proof state before:
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, 1 / 2 ^ N * 2 < ε
Tactic:
sorry
Proof state after:
no goals
Theorem: chineseMap_inj
Proof state before:
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
I : ι → Ideal R
⊢ Injective ⇑(chineseMap I)
Tactic:
rw [chineseMap, injective_lift_iff, ker_Pi_Quotient_mk]
Proof state after:
no goals
Theorem: isCoprime_Inf
Proof state before:
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : ι → Ideal R
s : Finset ι
hf : ∀ j ∈ s, IsCoprime I (J j)
⊢ IsCoprime I (⨅ j ∈ s, J j)
Tactic:
classical
simp_rw [isCoprime_iff_add] at *
induction s using Finset.induction with
| empty =>
    simp
| @insert i s _ hs =>
    rw [Finset.iInf_insert, inf_comm, one_eq_top, eq_top_iff, ← one_eq_top]
    set K := ⨅ j ∈ s, J j
    calc
      1 = I + K                  := (hs fun j hj ↦ hf j (Finset.mem_insert_of_mem hj)).symm
      _ = I + K * (I + J i)      := by rw [hf i (Finset.mem_insert_self i s), mul_one]
      _ = (1 + K) * I + K * J i  := by ring
      _ ≤ I + K ⊓ J i            := by gcongr ; apply mul_le_left ; apply mul_le_inf
Proof state after:
no goals
Theorem: isCoprime_Inf
Proof state before:
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : ι → Ideal R
s : Finset ι
hf : ∀ j ∈ s, IsCoprime I (J j)
⊢ IsCoprime I (⨅ j ∈ s, J j)
Tactic:
simp_rw [isCoprime_iff_add] at *
Proof state after:
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : ι → Ideal R
s : Finset ι
hf : ∀ j ∈ s, I + J j = 1
⊢ I + ⨅ j ∈ s, J j = 1
Theorem: isCoprime_Inf
Proof state before:
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : ι → Ideal R
s : Finset ι
hf : ∀ j ∈ s, I + J j = 1
⊢ I + ⨅ j ∈ s, J j = 1
Tactic:
induction s using Finset.induction with
| empty =>
    simp
| @insert i s _ hs =>
    rw [Finset.iInf_insert, inf_comm, one_eq_top, eq_top_iff, ← one_eq_top]
    set K := ⨅ j ∈ s, J j
    calc
      1 = I + K                  := (hs fun j hj ↦ hf j (Finset.mem_insert_of_mem hj)).symm
      _ = I + K * (I + J i)      := by rw [hf i (Finset.mem_insert_self i s), mul_one]
      _ = (1 + K) * I + K * J i  := by ring
      _ ≤ I + K ⊓ J i            := by gcongr ; apply mul_le_left ; apply mul_le_inf
Proof state after:
no goals
Theorem: isCoprime_Inf
Proof state before:
case empty
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : ι → Ideal R
hf : ∀ j ∈ ∅, I + J j = 1
⊢ I + ⨅ j ∈ ∅, J j = 1
Tactic:
simp
Proof state after:
no goals
Theorem: isCoprime_Inf
Proof state before:
case insert
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : i ∉ s
hs : (∀ j ∈ s, I + J j = 1) → I + ⨅ j ∈ s, J j = 1
hf : ∀ j ∈ insert i s, I + J j = 1
⊢ I + ⨅ j ∈ insert i s, J j = 1
Tactic:
rw [Finset.iInf_insert, inf_comm, one_eq_top, eq_top_iff, ← one_eq_top]
Proof state after:
case insert
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : i ∉ s
hs : (∀ j ∈ s, I + J j = 1) → I + ⨅ j ∈ s, J j = 1
hf : ∀ j ∈ insert i s, I + J j = 1
⊢ 1 ≤ I + (⨅ x ∈ s, J x) ⊓ J i
Theorem: isCoprime_Inf
Proof state before:
case insert
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : i ∉ s
hs : (∀ j ∈ s, I + J j = 1) → I + ⨅ j ∈ s, J j = 1
hf : ∀ j ∈ insert i s, I + J j = 1
⊢ 1 ≤ I + (⨅ x ∈ s, J x) ⊓ J i
Tactic:
set K := ⨅ j ∈ s, J j
Proof state after:
case insert
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : i ∉ s
hf : ∀ j ∈ insert i s, I + J j = 1
K : Ideal R := ⨅ j ∈ s, J j
hs : (∀ j ∈ s, I + J j = 1) → I + K = 1
⊢ 1 ≤ I + K ⊓ J i
Theorem: isCoprime_Inf
Proof state before:
case insert
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : i ∉ s
hf : ∀ j ∈ insert i s, I + J j = 1
K : Ideal R := ⨅ j ∈ s, J j
hs : (∀ j ∈ s, I + J j = 1) → I + K = 1
⊢ 1 ≤ I + K ⊓ J i
Tactic:
calc
  1 = I + K                  := (hs fun j hj ↦ hf j (Finset.mem_insert_of_mem hj)).symm
  _ = I + K * (I + J i)      := by rw [hf i (Finset.mem_insert_self i s), mul_one]
  _ = (1 + K) * I + K * J i  := by ring
  _ ≤ I + K ⊓ J i            := by gcongr ; apply mul_le_left ; apply mul_le_inf
Proof state after:
no goals
Theorem: isCoprime_Inf
Proof state before:
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : i ∉ s
hf : ∀ j ∈ insert i s, I + J j = 1
K : Ideal R := ⨅ j ∈ s, J j
hs : (∀ j ∈ s, I + J j = 1) → I + K = 1
⊢ I + K = I + K * (I + J i)
Tactic:
rw [hf i (Finset.mem_insert_self i s), mul_one]
Proof state after:
no goals
Theorem: isCoprime_Inf
Proof state before:
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : i ∉ s
hf : ∀ j ∈ insert i s, I + J j = 1
K : Ideal R := ⨅ j ∈ s, J j
hs : (∀ j ∈ s, I + J j = 1) → I + K = 1
⊢ I + K * (I + J i) = (1 + K) * I + K * J i
Tactic:
ring
Proof state after:
no goals
Theorem: isCoprime_Inf
Proof state before:
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : i ∉ s
hf : ∀ j ∈ insert i s, I + J j = 1
K : Ideal R := ⨅ j ∈ s, J j
hs : (∀ j ∈ s, I + J j = 1) → I + K = 1
⊢ (1 + K) * I + K * J i ≤ I + K ⊓ J i
Tactic:
gcongr
Proof state after:
case h₁
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : i ∉ s
hf : ∀ j ∈ insert i s, I + J j = 1
K : Ideal R := ⨅ j ∈ s, J j
hs : (∀ j ∈ s, I + J j = 1) → I + K = 1
⊢ (1 + K) * I ≤ I

case h₂
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : i ∉ s
hf : ∀ j ∈ insert i s, I + J j = 1
K : Ideal R := ⨅ j ∈ s, J j
hs : (∀ j ∈ s, I + J j = 1) → I + K = 1
⊢ K * J i ≤ K ⊓ J i
Theorem: isCoprime_Inf
Proof state before:
case h₁
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : i ∉ s
hf : ∀ j ∈ insert i s, I + J j = 1
K : Ideal R := ⨅ j ∈ s, J j
hs : (∀ j ∈ s, I + J j = 1) → I + K = 1
⊢ (1 + K) * I ≤ I

case h₂
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : i ∉ s
hf : ∀ j ∈ insert i s, I + J j = 1
K : Ideal R := ⨅ j ∈ s, J j
hs : (∀ j ∈ s, I + J j = 1) → I + K = 1
⊢ K * J i ≤ K ⊓ J i
Tactic:
apply mul_le_left
Proof state after:
case h₂
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : i ∉ s
hf : ∀ j ∈ insert i s, I + J j = 1
K : Ideal R := ⨅ j ∈ s, J j
hs : (∀ j ∈ s, I + J j = 1) → I + K = 1
⊢ K * J i ≤ K ⊓ J i
Theorem: isCoprime_Inf
Proof state before:
case h₂
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : i ∉ s
hf : ∀ j ∈ insert i s, I + J j = 1
K : Ideal R := ⨅ j ∈ s, J j
hs : (∀ j ∈ s, I + J j = 1) → I + K = 1
⊢ K * J i ≤ K ⊓ J i
Tactic:
apply mul_le_inf
Proof state after:
no goals
Theorem: chineseMap_surj
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
⊢ Surjective ⇑(chineseMap I)
Tactic:
intro g
Proof state after:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
⊢ ∃ a, (chineseMap I) a = g
Theorem: chineseMap_surj
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
⊢ ∃ a, (chineseMap I) a = g
Tactic:
choose f hf using fun i ↦ Ideal.Quotient.mk_surjective (g i)
Proof state after:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
⊢ ∃ a, (chineseMap I) a = g
Theorem: chineseMap_surj
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
key : ∀ (i : ι), ∃ e, (mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → (mk (I j)) e = 0
⊢ ∃ a, (chineseMap I) a = g
Tactic:
choose e he using key
Proof state after:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), (mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → (mk (I j)) (e i) = 0
⊢ ∃ a, (chineseMap I) a = g
Theorem: chineseMap_surj
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), (mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → (mk (I j)) (e i) = 0
⊢ ∃ a, (chineseMap I) a = g
Tactic:
use mk _ (∑ i, f i * e i)
Proof state after:
case h
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), (mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → (mk (I j)) (e i) = 0
⊢ (chineseMap I) ((mk (⨅ i, I i)) (∑ i : ι, f i * e i)) = g
Theorem: chineseMap_surj
Proof state before:
case h
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), (mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → (mk (I j)) (e i) = 0
⊢ (chineseMap I) ((mk (⨅ i, I i)) (∑ i : ι, f i * e i)) = g
Tactic:
ext i
Proof state after:
case h.h
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), (mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → (mk (I j)) (e i) = 0
i : ι
⊢ (chineseMap I) ((mk (⨅ i, I i)) (∑ i : ι, f i * e i)) i = g i
Theorem: chineseMap_surj
Proof state before:
case h.h
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), (mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → (mk (I j)) (e i) = 0
i : ι
⊢ (chineseMap I) ((mk (⨅ i, I i)) (∑ i : ι, f i * e i)) i = g i
Tactic:
rw [chineseMap_mk', map_sum, Fintype.sum_eq_single i]
Proof state after:
case h.h
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), (mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → (mk (I j)) (e i) = 0
i : ι
⊢ (mk (I i)) (f i * e i) = g i

case h.h
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), (mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → (mk (I j)) (e i) = 0
i : ι
⊢ ∀ (x : ι), x ≠ i → (mk (I i)) (f x * e x) = 0