internlm/Lean-Github huggingface dataset:
Theorem: MvPowerSeries.coeff_mul_prod_one_sub_of_lt_weightedOrder
Proof state before:
case refine'_2
σ : Type u_3
α✝ : Type ?u.62270
inst✝¹ : Semiring α✝
w : σ → ℕ
f✝ : MvPowerSeries σ α✝
α : Type u_1
ι : Type u_2
inst✝ : CommRing α
d : σ →₀ ℕ
s✝ : Finset ι
f : MvPowerSeries σ α
g : ι → MvPowerSeries σ α
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑((weight w) d) < weightedOrder w (g i)) → (coeff α d) (f * ∏ i ∈ s, (1 - g i)) = (coeff α d) f
t : ↑((weight w) d) < weightedOrder w (g a) ∧ ∀ a ∈ s, ↑((weight w) d) < weightedOrder w (g a)
⊢ (coeff α d) (f * ∏ i ∈ insert a s, (1 - g i)) = (coeff α d) f
Tactic:
rw [Finset.prod_insert ha, ← mul_assoc, mul_right_comm,
  coeff_mul_one_sub_of_lt_weightedOrder w _ t.1]
Proof state after:
case refine'_2
σ : Type u_3
α✝ : Type ?u.62270
inst✝¹ : Semiring α✝
w : σ → ℕ
f✝ : MvPowerSeries σ α✝
α : Type u_1
ι : Type u_2
inst✝ : CommRing α
d : σ →₀ ℕ
s✝ : Finset ι
f : MvPowerSeries σ α
g : ι → MvPowerSeries σ α
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑((weight w) d) < weightedOrder w (g i)) → (coeff α d) (f * ∏ i ∈ s, (1 - g i)) = (coeff α d) f
t : ↑((weight w) d) < weightedOrder w (g a) ∧ ∀ a ∈ s, ↑((weight w) d) < weightedOrder w (g a)
⊢ (coeff α d) (f * ∏ x ∈ s, (1 - g x)) = (coeff α d) f
Theorem: MvPowerSeries.coeff_mul_prod_one_sub_of_lt_weightedOrder
Proof state before:
case refine'_2
σ : Type u_3
α✝ : Type ?u.62270
inst✝¹ : Semiring α✝
w : σ → ℕ
f✝ : MvPowerSeries σ α✝
α : Type u_1
ι : Type u_2
inst✝ : CommRing α
d : σ →₀ ℕ
s✝ : Finset ι
f : MvPowerSeries σ α
g : ι → MvPowerSeries σ α
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑((weight w) d) < weightedOrder w (g i)) → (coeff α d) (f * ∏ i ∈ s, (1 - g i)) = (coeff α d) f
t : ↑((weight w) d) < weightedOrder w (g a) ∧ ∀ a ∈ s, ↑((weight w) d) < weightedOrder w (g a)
⊢ (coeff α d) (f * ∏ x ∈ s, (1 - g x)) = (coeff α d) f
Tactic:
exact ih t.2
Proof state after:
no goals
Theorem: MvPowerSeries.degree_apply
Proof state before:
σ : Type u_1
α : Type ?u.65991
inst✝ : Semiring α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ degree d = d.sum fun x => id
Tactic:
rw [degree, weight_apply]
Proof state after:
σ : Type u_1
α : Type ?u.65991
inst✝ : Semiring α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ (d.sum fun x => Mul.mul 1) = d.sum fun x => id
Theorem: MvPowerSeries.degree_apply
Proof state before:
σ : Type u_1
α : Type ?u.65991
inst✝ : Semiring α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ (d.sum fun x => Mul.mul 1) = d.sum fun x => id
Tactic:
apply congr_arg
Proof state after:
case h
σ : Type u_1
α : Type ?u.65991
inst✝ : Semiring α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ (fun x => Mul.mul 1) = fun x => id
Theorem: MvPowerSeries.degree_apply
Proof state before:
case h
σ : Type u_1
α : Type ?u.65991
inst✝ : Semiring α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ (fun x => Mul.mul 1) = fun x => id
Tactic:
ext _ n
Proof state after:
case h.h.h
σ : Type u_1
α : Type ?u.65991
inst✝ : Semiring α
f : MvPowerSeries σ α
d : σ →₀ ℕ
x✝ : σ
n : ℕ
⊢ Mul.mul 1 n = id n
Theorem: MvPowerSeries.degree_apply
Proof state before:
case h.h.h
σ : Type u_1
α : Type ?u.65991
inst✝ : Semiring α
f : MvPowerSeries σ α
d : σ →₀ ℕ
x✝ : σ
n : ℕ
⊢ Mul.mul 1 n = id n
Tactic:
have h_eq : Mul.mul 1 n = 1 * n := by rfl
Proof state after:
case h.h.h
σ : Type u_1
α : Type ?u.65991
inst✝ : Semiring α
f : MvPowerSeries σ α
d : σ →₀ ℕ
x✝ : σ
n : ℕ
h_eq : Mul.mul 1 n = 1 * n
⊢ Mul.mul 1 n = id n
Theorem: MvPowerSeries.degree_apply
Proof state before:
case h.h.h
σ : Type u_1
α : Type ?u.65991
inst✝ : Semiring α
f : MvPowerSeries σ α
d : σ →₀ ℕ
x✝ : σ
n : ℕ
h_eq : Mul.mul 1 n = 1 * n
⊢ Mul.mul 1 n = id n
Tactic:
rw [h_eq, id_eq, one_mul]
Proof state after:
no goals
Theorem: MvPowerSeries.degree_apply
Proof state before:
σ : Type u_1
α : Type ?u.65991
inst✝ : Semiring α
f : MvPowerSeries σ α
d : σ →₀ ℕ
x✝ : σ
n : ℕ
⊢ Mul.mul 1 n = 1 * n
Tactic:
rfl
Proof state after:
no goals
Theorem: MvPowerSeries.degree_eq_zero_iff
Proof state before:
σ : Type u_1
α : Type ?u.66556
inst✝ : Semiring α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ degree d = 0 ↔ d = 0
Tactic:
simp only [degree, weight, one_mul, AddMonoidHom.coe_mk, Finsupp.sum, Finset.sum_eq_zero_iff,
  Finsupp.mem_support_iff, _root_.not_imp_self, DFunLike.ext_iff, Finsupp.coe_zero, Pi.zero_apply,
  ZeroHom.coe_mk, Finset.sum_eq_zero_iff, Finsupp.mem_support_iff, ne_eq]
Proof state after:
no goals
Theorem: MvPowerSeries.le_degree
Proof state before:
σ : Type u_1
α : Type ?u.68078
inst✝ : Semiring α
f : MvPowerSeries σ α
x : σ
d : σ →₀ ℕ
⊢ d x ≤ degree d
Tactic:
convert le_weight _ x _ d
Proof state after:
case convert_2
σ : Type u_1
α : Type ?u.68078
inst✝ : Semiring α
f : MvPowerSeries σ α
x : σ
d : σ →₀ ℕ
⊢ 1 ≠ 0
Theorem: MvPowerSeries.le_degree
Proof state before:
case convert_2
σ : Type u_1
α : Type ?u.68078
inst✝ : Semiring α
f : MvPowerSeries σ α
x : σ
d : σ →₀ ℕ
⊢ 1 ≠ 0
Tactic:
exact NeZero.ne 1
Proof state after:
no goals
Theorem: MvPowerSeries.finite_of_degree_le
Proof state before:
σ : Type u_1
α : Type ?u.69196
inst✝¹ : Semiring α
f : MvPowerSeries σ α
inst✝ : Finite σ
n : ℕ
⊢ {f | degree f ≤ n}.Finite
Tactic:
refine' finite_of_weight_le (Function.const σ 1) _ n
Proof state after:
σ : Type u_1
α : Type ?u.69196
inst✝¹ : Semiring α
f : MvPowerSeries σ α
inst✝ : Finite σ
n : ℕ
⊢ ∀ (x : σ), Function.const σ 1 x ≠ 0
Theorem: MvPowerSeries.finite_of_degree_le
Proof state before:
σ : Type u_1
α : Type ?u.69196
inst✝¹ : Semiring α
f : MvPowerSeries σ α
inst✝ : Finite σ
n : ℕ
⊢ ∀ (x : σ), Function.const σ 1 x ≠ 0
Tactic:
intro _
Proof state after:
σ : Type u_1
α : Type ?u.69196
inst✝¹ : Semiring α
f : MvPowerSeries σ α
inst✝ : Finite σ
n : ℕ
x✝ : σ
⊢ Function.const σ 1 x✝ ≠ 0
Theorem: MvPowerSeries.finite_of_degree_le
Proof state before:
σ : Type u_1
α : Type ?u.69196
inst✝¹ : Semiring α
f : MvPowerSeries σ α
inst✝ : Finite σ
n : ℕ
x✝ : σ
⊢ Function.const σ 1 x✝ ≠ 0
Tactic:
simp only [Function.const_apply, ne_eq, one_ne_zero, not_false_eq_true]
Proof state after:
no goals
Theorem: ContinuousAlgHom.coe_injective
Proof state before:
R : Type u_1
inst✝⁹ : CommSemiring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSemiring R
A : Type u_2
inst✝⁶ : Semiring A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSemiring A
B : Type u_3
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ Injective toAlgHom
Tactic:
intro f g H
Proof state after:
R : Type u_1
inst✝⁹ : CommSemiring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSemiring R
A : Type u_2
inst✝⁶ : Semiring A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSemiring A
B : Type u_3
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A →A[R] B
H : ↑f = ↑g
⊢ f = g
Theorem: ContinuousAlgHom.coe_injective
Proof state before:
R : Type u_1
inst✝⁹ : CommSemiring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSemiring R
A : Type u_2
inst✝⁶ : Semiring A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSemiring A
B : Type u_3
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A →A[R] B
H : ↑f = ↑g
⊢ f = g
Tactic:
cases f
Proof state after:
case mk
R : Type u_1
inst✝⁹ : CommSemiring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSemiring R
A : Type u_2
inst✝⁶ : Semiring A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSemiring A
B : Type u_3
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
g : A →A[R] B
toAlgHom✝ : A →ₐ[R] B
cont✝ : Continuous (↑↑toAlgHom✝.toRingHom).toFun
H : ↑{ toAlgHom := toAlgHom✝, cont := cont✝ } = ↑g
⊢ { toAlgHom := toAlgHom✝, cont := cont✝ } = g
Theorem: ContinuousAlgHom.coe_injective
Proof state before:
case mk
R : Type u_1
inst✝⁹ : CommSemiring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSemiring R
A : Type u_2
inst✝⁶ : Semiring A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSemiring A
B : Type u_3
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
g : A →A[R] B
toAlgHom✝ : A →ₐ[R] B
cont✝ : Continuous (↑↑toAlgHom✝.toRingHom).toFun
H : ↑{ toAlgHom := toAlgHom✝, cont := cont✝ } = ↑g
⊢ { toAlgHom := toAlgHom✝, cont := cont✝ } = g
Tactic:
cases g
Proof state after:
case mk.mk
R : Type u_1
inst✝⁹ : CommSemiring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSemiring R
A : Type u_2
inst✝⁶ : Semiring A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSemiring A
B : Type u_3
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
toAlgHom✝¹ : A →ₐ[R] B
cont✝¹ : Continuous (↑↑toAlgHom✝¹.toRingHom).toFun
toAlgHom✝ : A →ₐ[R] B
cont✝ : Continuous (↑↑toAlgHom✝.toRingHom).toFun
H : ↑{ toAlgHom := toAlgHom✝¹, cont := cont✝¹ } = ↑{ toAlgHom := toAlgHom✝, cont := cont✝ }
⊢ { toAlgHom := toAlgHom✝¹, cont := cont✝¹ } = { toAlgHom := toAlgHom✝, cont := cont✝ }
Theorem: ContinuousAlgHom.coe_injective
Proof state before:
case mk.mk
R : Type u_1
inst✝⁹ : CommSemiring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSemiring R
A : Type u_2
inst✝⁶ : Semiring A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSemiring A
B : Type u_3
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
toAlgHom✝¹ : A →ₐ[R] B
cont✝¹ : Continuous (↑↑toAlgHom✝¹.toRingHom).toFun
toAlgHom✝ : A →ₐ[R] B
cont✝ : Continuous (↑↑toAlgHom✝.toRingHom).toFun
H : ↑{ toAlgHom := toAlgHom✝¹, cont := cont✝¹ } = ↑{ toAlgHom := toAlgHom✝, cont := cont✝ }
⊢ { toAlgHom := toAlgHom✝¹, cont := cont✝¹ } = { toAlgHom := toAlgHom✝, cont := cont✝ }
Tactic:
congr
Proof state after:
no goals
Theorem: ContinuousAlgHom.ext_ring
Proof state before:
R : Type u_1
inst✝¹⁰ : CommSemiring R
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSemiring R
A : Type u_2
inst✝⁷ : Semiring A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : TopologicalSemiring A
B : Type u_3
inst✝⁴ : Semiring B
inst✝³ : TopologicalSpace B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : TopologicalSpace R
f g : R →A[R] A
⊢ f = g
Tactic:
apply coe_inj.1
Proof state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSemiring R
A : Type u_2
inst✝⁷ : Semiring A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : TopologicalSemiring A
B : Type u_3
inst✝⁴ : Semiring B
inst✝³ : TopologicalSpace B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : TopologicalSpace R
f g : R →A[R] A
⊢ ↑f = ↑g
Theorem: ContinuousAlgHom.ext_ring
Proof state before:
R : Type u_1
inst✝¹⁰ : CommSemiring R
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSemiring R
A : Type u_2
inst✝⁷ : Semiring A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : TopologicalSemiring A
B : Type u_3
inst✝⁴ : Semiring B
inst✝³ : TopologicalSpace B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : TopologicalSpace R
f g : R →A[R] A
⊢ ↑f = ↑g
Tactic:
apply Algebra.ext_id
Proof state after:
no goals
Theorem: DenseRange.topologicalClosure_map_submodule'
Proof state before:
R : Type u_1
inst✝¹³ : CommSemiring R
inst✝¹² : TopologicalSpace R
inst✝¹¹ : TopologicalSemiring R
A : Type u_2
inst✝¹⁰ : Semiring A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSemiring A
B : Type u_3
inst✝⁷ : Semiring B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : TopologicalSpace R
inst✝² : ContinuousAdd A
inst✝¹ : ContinuousSMul R B
inst✝ : ContinuousAdd B
f : A →A[R] B
hf' : DenseRange ⇑f
s : Submodule R A
hs : s.topologicalClosure = ⊤
⊢ (Submodule.map (↑f) s).topologicalClosure = ⊤
Tactic:
rw [SetLike.ext'_iff] at hs ⊢
Proof state after:
R : Type u_1
inst✝¹³ : CommSemiring R
inst✝¹² : TopologicalSpace R
inst✝¹¹ : TopologicalSemiring R
A : Type u_2
inst✝¹⁰ : Semiring A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSemiring A
B : Type u_3
inst✝⁷ : Semiring B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : TopologicalSpace R
inst✝² : ContinuousAdd A
inst✝¹ : ContinuousSMul R B
inst✝ : ContinuousAdd B
f : A →A[R] B
hf' : DenseRange ⇑f
s : Submodule R A
hs : ↑s.topologicalClosure = ↑⊤
⊢ ↑(Submodule.map (↑f) s).topologicalClosure = ↑⊤
Theorem: DenseRange.topologicalClosure_map_submodule'
Proof state before:
R : Type u_1
inst✝¹³ : CommSemiring R
inst✝¹² : TopologicalSpace R
inst✝¹¹ : TopologicalSemiring R
A : Type u_2
inst✝¹⁰ : Semiring A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSemiring A
B : Type u_3
inst✝⁷ : Semiring B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : TopologicalSpace R
inst✝² : ContinuousAdd A
inst✝¹ : ContinuousSMul R B
inst✝ : ContinuousAdd B
f : A →A[R] B
hf' : DenseRange ⇑f
s : Submodule R A
hs : ↑s.topologicalClosure = ↑⊤
⊢ ↑(Submodule.map (↑f) s).topologicalClosure = ↑⊤
Tactic:
simp only [Submodule.topologicalClosure_coe, Submodule.top_coe, ← dense_iff_closure_eq] at hs ⊢
Proof state after:
R : Type u_1
inst✝¹³ : CommSemiring R
inst✝¹² : TopologicalSpace R
inst✝¹¹ : TopologicalSemiring R
A : Type u_2
inst✝¹⁰ : Semiring A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSemiring A
B : Type u_3
inst✝⁷ : Semiring B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : TopologicalSpace R
inst✝² : ContinuousAdd A
inst✝¹ : ContinuousSMul R B
inst✝ : ContinuousAdd B
f : A →A[R] B
hf' : DenseRange ⇑f
s : Submodule R A
hs : Dense ↑s
⊢ Dense ↑(Submodule.map (↑f) s)
Theorem: DenseRange.topologicalClosure_map_submodule'
Proof state before:
R : Type u_1
inst✝¹³ : CommSemiring R
inst✝¹² : TopologicalSpace R
inst✝¹¹ : TopologicalSemiring R
A : Type u_2
inst✝¹⁰ : Semiring A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSemiring A
B : Type u_3
inst✝⁷ : Semiring B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : TopologicalSpace R
inst✝² : ContinuousAdd A
inst✝¹ : ContinuousSMul R B
inst✝ : ContinuousAdd B
f : A →A[R] B
hf' : DenseRange ⇑f
s : Submodule R A
hs : Dense ↑s
⊢ Dense ↑(Submodule.map (↑f) s)
Tactic:
exact hf'.dense_image f.continuous hs
Proof state after:
no goals
Theorem: ContinuousAlgHom.coe_eq_id
Proof state before:
R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSemiring R
A : Type u_2
inst✝³ : Semiring A
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSemiring A
inst✝ : Algebra R A
f : A →A[R] A
⊢ ↑f = AlgHom.id R A ↔ f = id R A
Tactic:
rw [← coe_id, coe_inj]
Proof state after:
no goals
Theorem: Ideal.pow_eq_bot
Proof state before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I : Ideal R
n : ℕ
hn : n ≠ 0
⊢ I ^ n = ⊥ ↔ I = ⊥
Tactic:
induction' n with n ih
Proof state after:
case zero
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I : Ideal R
hn : 0 ≠ 0
⊢ I ^ 0 = ⊥ ↔ I = ⊥

case succ
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I : Ideal R
n : ℕ
ih : n ≠ 0 → (I ^ n = ⊥ ↔ I = ⊥)
hn : n + 1 ≠ 0
⊢ I ^ (n + 1) = ⊥ ↔ I = ⊥
Theorem: Ideal.pow_eq_bot
Proof state before:
case zero
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I : Ideal R
hn : 0 ≠ 0
⊢ I ^ 0 = ⊥ ↔ I = ⊥
Tactic:
exfalso
Proof state after:
case zero
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I : Ideal R
hn : 0 ≠ 0
⊢ False
Theorem: Ideal.pow_eq_bot
Proof state before:
case zero
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I : Ideal R
hn : 0 ≠ 0
⊢ False
Tactic:
exact hn (Eq.refl _)
Proof state after:
no goals
Theorem: Ideal.pow_eq_bot
Proof state before:
case succ
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I : Ideal R
n : ℕ
ih : n ≠ 0 → (I ^ n = ⊥ ↔ I = ⊥)
hn : n + 1 ≠ 0
⊢ I ^ (n + 1) = ⊥ ↔ I = ⊥
Tactic:
by_cases hn0 : n = 0
Proof state after:
case pos
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I : Ideal R
n : ℕ
ih : n ≠ 0 → (I ^ n = ⊥ ↔ I = ⊥)
hn : n + 1 ≠ 0
hn0 : n = 0
⊢ I ^ (n + 1) = ⊥ ↔ I = ⊥

case neg
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I : Ideal R
n : ℕ
ih : n ≠ 0 → (I ^ n = ⊥ ↔ I = ⊥)
hn : n + 1 ≠ 0
hn0 : ¬n = 0
⊢ I ^ (n + 1) = ⊥ ↔ I = ⊥
Theorem: Ideal.pow_eq_bot
Proof state before:
case pos
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I : Ideal R
n : ℕ
ih : n ≠ 0 → (I ^ n = ⊥ ↔ I = ⊥)
hn : n + 1 ≠ 0
hn0 : n = 0
⊢ I ^ (n + 1) = ⊥ ↔ I = ⊥
Tactic:
rw [hn0, pow_one]
Proof state after:
no goals
Theorem: Ideal.pow_eq_bot
Proof state before:
case neg
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I : Ideal R
n : ℕ
ih : n ≠ 0 → (I ^ n = ⊥ ↔ I = ⊥)
hn : n + 1 ≠ 0
hn0 : ¬n = 0
⊢ I ^ (n + 1) = ⊥ ↔ I = ⊥
Tactic:
rw [pow_succ, mul_eq_bot, ih hn0, or_self_iff]
Proof state after:
no goals
Theorem: MvPolynomial.eval₂Hom.smul
Proof state before:
R : Type u_2
S : Type u_1
σ : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
r : R
P : MvPolynomial σ R
⊢ (eval₂Hom f g) (r • P) = f r • (eval₂Hom f g) P
Tactic:
simp only [smul_eq_C_mul, coe_eval₂Hom, eval₂_mul, eval₂_C, Algebra.id.smul_eq_mul]
Proof state after:
no goals
Theorem: quotient_mk_eq_ofRel
Proof state before:
A : Type u_1
inst✝ : CommRing A
r : A → A → Prop
a b : A
h : r a b
⊢ (Ideal.Quotient.mk (ofRel r)) a = (Ideal.Quotient.mk (ofRel r)) b
Tactic:
suffices hinj : Function.Injective (RingQuot.ringQuotEquivIdealQuotient r).invFun by
  apply hinj; exact mkRingHom_rel h
Proof state after:
A : Type u_1
inst✝ : CommRing A
r : A → A → Prop
a b : A
h : r a b
⊢ Function.Injective (ringQuotEquivIdealQuotient r).invFun
Theorem: quotient_mk_eq_ofRel
Proof state before:
A : Type u_1
inst✝ : CommRing A
r : A → A → Prop
a b : A
h : r a b
⊢ Function.Injective (ringQuotEquivIdealQuotient r).invFun
Tactic:
rw [Function.injective_iff_hasLeftInverse]
Proof state after:
A : Type u_1
inst✝ : CommRing A
r : A → A → Prop
a b : A
h : r a b
⊢ Function.HasLeftInverse (ringQuotEquivIdealQuotient r).invFun
Theorem: quotient_mk_eq_ofRel
Proof state before:
A : Type u_1
inst✝ : CommRing A
r : A → A → Prop
a b : A
h : r a b
⊢ Function.HasLeftInverse (ringQuotEquivIdealQuotient r).invFun
Tactic:
exact ⟨(ringQuotEquivIdealQuotient r).toFun, (ringQuotEquivIdealQuotient r).right_inv⟩
Proof state after:
no goals
Theorem: quotient_mk_eq_ofRel
Proof state before:
A : Type u_1
inst✝ : CommRing A
r : A → A → Prop
a b : A
h : r a b
hinj : Function.Injective (ringQuotEquivIdealQuotient r).invFun
⊢ (Ideal.Quotient.mk (ofRel r)) a = (Ideal.Quotient.mk (ofRel r)) b
Tactic:
apply hinj
Proof state after:
case a
A : Type u_1
inst✝ : CommRing A
r : A → A → Prop
a b : A
h : r a b
hinj : Function.Injective (ringQuotEquivIdealQuotient r).invFun
⊢ (ringQuotEquivIdealQuotient r).invFun ((Ideal.Quotient.mk (ofRel r)) a) =
    (ringQuotEquivIdealQuotient r).invFun ((Ideal.Quotient.mk (ofRel r)) b)
Theorem: quotient_mk_eq_ofRel
Proof state before:
case a
A : Type u_1
inst✝ : CommRing A
r : A → A → Prop
a b : A
h : r a b
hinj : Function.Injective (ringQuotEquivIdealQuotient r).invFun
⊢ (ringQuotEquivIdealQuotient r).invFun ((Ideal.Quotient.mk (ofRel r)) a) =
    (ringQuotEquivIdealQuotient r).invFun ((Ideal.Quotient.mk (ofRel r)) b)
Tactic:
exact mkRingHom_rel h
Proof state after:
no goals
Theorem: Ideal.quotient_mk_eq_ringQuot_apply
Proof state before:
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
r : A → A → Prop
a : A
⊢ (Quotient.mk (ofRel r)) a = (ringQuotToIdealQuotient r) ((mkAlgHom R r) a)
Tactic:
rw [← ringQuotToIdealQuotient_apply r a, ← mkAlgHom_coe R r]
Proof state after:
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
r : A → A → Prop
a : A
⊢ (ringQuotToIdealQuotient r) (↑(mkAlgHom R r) a) = (ringQuotToIdealQuotient r) ((mkAlgHom R r) a)
Theorem: Ideal.quotient_mk_eq_ringQuot_apply
Proof state before:
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
r : A → A → Prop
a : A
⊢ (ringQuotToIdealQuotient r) (↑(mkAlgHom R r) a) = (ringQuotToIdealQuotient r) ((mkAlgHom R r) a)
Tactic:
rfl
Proof state after:
no goals
Theorem: Ideal.Quotient.rel_le_ker
Proof state before:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
r : R → R → Prop
hr : I = ofRel r
f : R →+* S
hf : ∀ {a b : R}, r a b → f a = f b
⊢ I ≤ RingHom.ker f
Tactic:
rw [hr, ofRel, Submodule.span_le]
Proof state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
r : R → R → Prop
hr : I = ofRel r
f : R →+* S
hf : ∀ {a b : R}, r a b → f a = f b
⊢ {x | ∃ a b, r a b ∧ x + b = a} ⊆ ↑(RingHom.ker f)
Theorem: Ideal.Quotient.rel_le_ker
Proof state before:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
r : R → R → Prop
hr : I = ofRel r
f : R →+* S
hf : ∀ {a b : R}, r a b → f a = f b
⊢ {x | ∃ a b, r a b ∧ x + b = a} ⊆ ↑(RingHom.ker f)
Tactic:
rintro x ⟨a, b, hx, hab⟩
Proof state after:
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
r : R → R → Prop
hr : I = ofRel r
f : R →+* S
hf : ∀ {a b : R}, r a b → f a = f b
x a b : R
hx : r a b
hab : x + b = a
⊢ x ∈ ↑(RingHom.ker f)
Theorem: Ideal.Quotient.rel_le_ker
Proof state before:
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
r : R → R → Prop
hr : I = ofRel r
f : R →+* S
hf : ∀ {a b : R}, r a b → f a = f b
x a b : R
hx : r a b
hab : x + b = a
⊢ x ∈ ↑(RingHom.ker f)
Tactic:
rw [eq_sub_iff_add_eq.mpr hab, SetLike.mem_coe, RingHom.mem_ker, map_sub, sub_eq_zero, hf hx]
Proof state after:
no goals
Theorem: TrivSqZeroExt.mem_kerIdeal_iff_inr
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
x : TrivSqZeroExt R M
⊢ x ∈ kerIdeal R M ↔ x = inr x.snd
Tactic:
obtain ⟨r, m⟩ := x
Proof state after:
case mk
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
r : R
m : M
⊢ (r, m) ∈ kerIdeal R M ↔ (r, m) = inr (snd (r, m))
Theorem: TrivSqZeroExt.mem_kerIdeal_iff_inr
Proof state before:
case mk
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
r : R
m : M
⊢ (r, m) ∈ kerIdeal R M ↔ (r, m) = inr (snd (r, m))
Tactic:
simp only [kerIdeal, RingHom.mem_ker, fstHom_apply, fst_mk]
Proof state after:
case mk
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
r : R
m : M
⊢ r = 0 ↔ (r, m) = inr (snd (r, m))
Theorem: TrivSqZeroExt.mem_kerIdeal_iff_inr
Proof state before:
case mk
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
r : R
m : M
⊢ r = 0 ↔ (r, m) = inr (snd (r, m))
Tactic:
exact ⟨fun hr => by rw [hr]; rfl, fun hrm => by rw [← fst_mk r m, hrm, fst_inr]⟩
Proof state after:
no goals
Theorem: TrivSqZeroExt.mem_kerIdeal_iff_inr
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
r : R
m : M
hr : r = 0
⊢ (r, m) = inr (snd (r, m))
Tactic:
rw [hr]
Proof state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
r : R
m : M
hr : r = 0
⊢ (0, m) = inr (snd (0, m))
Theorem: TrivSqZeroExt.mem_kerIdeal_iff_inr
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
r : R
m : M
hr : r = 0
⊢ (0, m) = inr (snd (0, m))
Tactic:
rfl
Proof state after:
no goals
Theorem: TrivSqZeroExt.mem_kerIdeal_iff_inr
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
r : R
m : M
hrm : (r, m) = inr (snd (r, m))
⊢ r = 0
Tactic:
rw [← fst_mk r m, hrm, fst_inr]
Proof state after:
no goals
Theorem: TrivSqZeroExt.mem_kerIdeal_iff_exists
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
x : TrivSqZeroExt R M
⊢ x ∈ kerIdeal R M ↔ ∃ m, x = inr m
Tactic:
rw [mem_kerIdeal_iff_inr]
Proof state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
x : TrivSqZeroExt R M
⊢ x = inr x.snd ↔ ∃ m, x = inr m